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