Stream: Beginner Questions

Topic: How to approach this formalization

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Sep 25 2022 at 22:23 UTC