Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error

On 1/18/2013 1:33 AM, Lars Noschinski wrote:
On 18.01.2013 05:35, Gottfried Barrow wrote:
primrec sFOLf :: "sFOLdt => bool" where
"sFOLf (In u1 u2) = (u1 inS u2)" |
"sFOLf (And f1 f2) = ((sFOLf (Rec f1)) & (sFOLf (Rec f2)))" |
"sFOLf (Rec f) = True"

This definition is not primitive recursive and hence rejected by primrec (recursive calls my only make the arguments structurally smaller, so "sFOLf (Rec f1)" is not valid on the rhs.

That was my experimental effort to force some termination; from that and some other ideas, I figured out I was too far off to stumble on to something that would make it all work.

However, it's not obvious to me why "sFOLf (Rec f1)" is not smaller. No matter what "f1" is, it looks like I should get ""sFOLf (Rec f1) = True" on the second call of sFOLf.

On the other hand, "((sFOLf (Rec f1)) & (sFOLf (Rec f2)))" starts out as "bool & bool", and it ends up as "bool & bool", even with the recursive calls, so I guess that wouldn't be considered "structurally smaller". It would help if I had a more precise understanding of "structurally smaller", but I don't worry about that right now.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.