[isabelle-dev] functions over abstract data

[Alexander Krauss]

Hi Chris,

[...]

> 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
http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.pdf 
?
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 
"one-man-feature".


> 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.

Alex