
24 Feb
2013
24 Feb
'13
7:39 a.m.
* Kim-Ee Yeoh
On Sun, Feb 24, 2013 at 7:09 PM, Roman Cheplyaka
wrote: Thus, your recursion is well-founded — you enter the recursion with the input strictly smaller than you had in the beginning.
Perhaps you meant /productive/ corecursion?
Because the definition "A ::= B A" you gave is codata.
It is just a grammar production, which I chose to interpret recursively. Whether it's productive when interpreted corecursively depends on the particular interpretation, I guess, and may not actually depend on factors like left recursion. I haven't thought about it much. Roman