Eric Bond (Aug 30 2021 at 17:31): Eric Bond (Aug 30 2021 at 17:31):Is there a way to hack PHOAS into Isabelle HOL? I know the well known encodings heavily rely on dependent types, but I've seen some folks pull off hackery with Locales in similar situations.
I'd like to encode something simple like
https://gist.github.com/bond15/8a7c265f4e78ee88ee361425b582a1bb
Wolfgang Jeltsch (Sep 01 2021 at 13:15):Why exactly would you need dependent types? For handling contexts or for something else?
If it’s the former, then you can just decide to have an infinite list of additional variables around, by which you turn the type of variable indices from Fin n into Fin n + ℕ, which is isomorphic to ℕ. Instead of a finite list of variable assignments, whose length depends on the nesting depth of binders, you then have an infinite list of variable assignments.
This is the approach we’ve come up with for the implementation of the Þ-calculus (see https://github.com/input-output-hk/ouroboros-high-assurance).
Eric Bond (Sep 01 2021 at 15:47):from that description, Isn't that a FOAS encoding? I'd like to leverage the host language for variable binding and substitution instead of explicitly managing a context of variables.
I'm curious to see the example but I'm not sure where to look in that repo :).
Wolfgang Jeltsch (Sep 01 2021 at 16:33):When speaking about contexts, I didn’t mean that they are represented by first-class entities in the encoding but rather that they exist as a concept, which we represent indirectly using HOAS. In HOAS, you can represent an open term (a term that may contain free variables) as a function with domain Fin n a, where a is the type of values assigned to variables. We represent such a term as a function with domain Stream a. The intuition is that beside the variables bound by surrounding binders we may have infinitely many other variables, of which you can think as global variables.
You may want to have a look at https://github.com/input-output-hk/ouroboros-high-assurance/blob/master/Isabelle/Thorn_Calculus/Thorn_Calculus-Processes.thy. This theory defines an algebraic data type process, whose values are HOAS encodings of closed terms. It then uses the type process family to represent open terms, where 'a family is a synonym of chan stream ⇒ 'a (chan is the type of things assigned to variables).
The semantics defined in https://github.com/input-output-hk/ouroboros-high-assurance/blob/master/Isabelle/Thorn_Calculus/Thorn_Calculus-Semantics-Synchronous.thy as the relation synchronous_transition is based on process family. It handles the introduction of new local variables by switching from an original environment e :: chan stream to an extended environment a ## e :: chan stream, where a is the value assigned to the local variable.
Last updated: Apr 16 2024 at 12:28 UTC