[isabelle-dev] functions over abstract data
krauss at in.tum.de
Sat Aug 24 23:20:19 CEST 2013
> When defining a function "f", whose result type is "T", it might be
> necessary to "peek under the hood" in order to show termination. When
> doing this manually, we destroy the abstraction and always have to
> reason about the raw-level and even worse, also all the existing
> constants with result type T have to be deconstructed in the definition.
I discussed similar ideas with John Matthews around 2007/8, where we
also had a recursive specification of a value that could "internally" be
expressed as a recursive function, even though it was not of function
type itself. The (single) motivation at the time was the attempt to
define infinite streams, modelled basically as "nat => 'a". However, I
abandoned the approach as too complicated. For streams, I believe they
should be more naturally defined corecursively. The same might hold for
your parsers if you find a good way of expressing it: Your "par"
definition is well-formed because the recursive call is wrapped into
something else... This looks more like a productivity argument then a
termination one, even though, when unfolding, one can be seen as the other.
Do you know the work of Nils Anders Danielsson on parsers, in particular
I'm not sure what this would mean in HOL, but it is certainly relevant.
> Here comes my suggestion
What you are proposing would add substantial complexity to pretty much
everything in the function package. While it might be possible to do
such a thing ("no obvious deficiencies"), you would pay later when
maintaining the stuff. This is too much for what seems to me like a
> PS: I started to dive into the function package. My first hurdle is that
> for "f" not of function type (as in "par"), no recursive calls are
> generated, since "Function_Ctx_Tree.mk_tree" says that "No cong rules
> could be found".
The analysis in the function package assumes basically a form where the
arguments of recursive calls can be extracted explicitly. This is a hard
assumption, and I see no chance of getting rid of it. The only sensible
way of lifting this restriction is to build some sort of wrapper that
reduces some other format to a normal function definition.
More information about the isabelle-dev