[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)
uuomul at yahoo.com
Tue Aug 6 12:12:48 CEST 2013
Many thanks for your enthusiasm!
> I'd like to learn about corecursion up-to, which I have not come across so
> far. Are there any good references for this?
A good early account of the up-to techniques at the level of generality we are interested in is Bartels's
There have been many later developments, including very recent work by Stefan Milius:
(see there "Abstract GSOS rules and a Modular Treatment of Recursive Definitions")
>> Or should I rather have a beer with Andrei?
Yes, let us definitely have a beer.
Corec-up-to seems to mesh well with the function package.
For now, what we can handle are function definitions such as the following, where nat_stream
is the type of streams of naturals, + is either nat addition or componentwise nat-stream addition,
and SCons is "stream cons".
f : nat -> nat_stream
n > 10 ==> f n = f (n - 1) + SCons (f (n + 17))
n <= 10 ==> f n = SCons (f (n + 13)) + SCons (f (n + 11) + f n)
With the function package, we find that all (co)recursive calls become eventually guarded (in a properly uniform context),
and then use corec-upto.
Jasmin has ideas on how to go way beyond this, but let's see if "LCF" can keep up with him. :-)
More information about the isabelle-dev