Email Gateway (Aug 23 2022 at 09:09): Email Gateway (Aug 23 2022 at 09:09):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
I interpret that you want to have an algorithm that given two terms s and t, you want to decide whether s >KBO t holds,
where also all parameters of KBO are provided.
Yes, such an algorithm is available. In fact, “kbo” in Isabelle is directly defined as an executable function
of type “term -> term -> (bool,bool)” where the two Booleans indicate whether the terms are in >KBO or in >=KBO relation.
Best regards,
René
signature.asc
Email Gateway (Aug 23 2022 at 09:11):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Hi Jens,
well definitely such a generator is not part of the AFP-entry.
Note that for KBO, it necessarily must return some infinite list or sequence.
E.g., consider a signature with symbol 0(unary), 1(constant), 2(constant) which all have their own weight,
and where 1 is highest in precedence.
Then in KBO we have
2 > 1
2 > 0(1)
2 > 0(0(1))
2 > …
so for reducing 2, you have to produce the infinite list 1, 0(1), 0(0(1)), …
Best,
René
signature.asc
Last updated: May 07 2024 at 20:13 UTC