waynee95 (Feb 03 2022 at 22:52): waynee95 (Feb 03 2022 at 22:52):I am currently working on my first formalization of a paper in Isabelle. But I am not sure how I can model the following terms as a datatype within Isabelle. The terms are basically an extended version of how terms look in lambda calculus. So we have abstraction and application. There are also some operators but I now how to model them.
The point where I get stuck is that everything is in the context of a complete lattice. So we consider some complete lattice M and then a set of functions on that lattice. And each of those functions would be allowed as a term too.
Mathias Fleury (Feb 04 2022 at 06:34):I would add a Lattice_Operation f constructor where f is any function with the correct type. Then I would define a predicate stating that the term is well founded iff f is in the set of functions on the lattice.
Mathias Fleury (Feb 04 2022 at 06:35):If your functions have many different types, this is going to be ugly however. Or it will not work if you have infinitely many types.
Last updated: Apr 23 2024 at 20:15 UTC