------------------------------------------------------------------------ -- An investigation of various ways to define the semantics of an -- untyped λ-calculus and a virtual machine, and a discussion of -- type soundness and compiler correctness -- -- Nils Anders Danielsson ------------------------------------------------------------------------ module Lambda where -- Syntax and type system for an untyped λ-calculus. import Lambda.Syntax ------------------------------------------------------------------------ -- Semantics based on substitutions -- Substitutions. import Lambda.Substitution -- A big-step semantics for the language. Conditional coinduction is -- used to avoid duplication of rules. -- -- Cousot and Cousot give a similar definition in "Bi-inductive -- structural semantics", and their definition inspired this one. -- Their definition has almost the same rules, but these rules are -- interpreted in the framework of bi-induction rather than the -- framework of mixed induction and (conditional) coinduction. import Lambda.Substitution.OneSemantics -- Two separate semantics for the language, one for converging terms -- and the other for diverging terms, as given by Leroy and Grall in -- "Coinductive big-step operational semantics". -- -- Leroy and Grall attempted to unify their two semantics into a -- single one, using only coinduction, but failed to find a definition -- which was equivalent to the two that they started with. However, -- they aimed for a definition which did not have more rules than the -- definition for converging terms; the definition in OneSemantics -- does not satisfy this criterion. import Lambda.Substitution.TwoSemantics -- The two definitions are equivalent. import Lambda.Substitution.Equivalence -- A functional semantics, along with a type soundness proof. import Lambda.Substitution.Functional ------------------------------------------------------------------------ -- Virtual machine -- A virtual machine with two semantics (one relational and one -- functional), a compiler from the λ-calculus defined above into the -- language of the virtual machine, and a proof showing that the two -- semantics are equivalent. import Lambda.VirtualMachine ------------------------------------------------------------------------ -- Semantics based on closures -- A semantics for the untyped λ-calculus, based on closures and -- environments, as given by Leroy and Grall in "Coinductive big-step -- operational semantics" (more or less). -- -- The module also contains a proof which shows that the compiler in -- Lambda.VirtualMachine preserves the semantics (assuming that the -- virtual machine is deterministic). Leroy and Grall prove almost the -- same thing. In their proof they use a relation indexed by a natural -- number to work around limitations in Coq's productivity checker. -- Agda has similar limitations, but I work around them using mixed -- induction/coinduction, which in my opinion is more elegant. I am -- not sure if my workaround would work in Coq, though. import Lambda.Closure.Relational -- A semantics for the untyped λ-calculus which uses the partiality -- monad, along with another compiler correctness proof. An advantage -- of formulating the semantics in this way is that it is very easy to -- state compiler correctness. import Lambda.Closure.Functional -- The module above uses some workarounds in order to convince Agda -- that the code is productive. The following module contains (more or -- less) the same code without the workarounds, but is checked with -- the termination checker turned off. import Lambda.Closure.Functional.No-workarounds -- The relational and functional semantics are equivalent. import Lambda.Closure.Equivalence -- An alternative definition of the functional semantics. This -- definition uses continuation-passing style instead of bind. import Lambda.Closure.Functional.Alternative -- A definition of a type system (with recursive types) for the -- λ-calculus given above, and a proof of type soundness for the -- functional semantics. import Lambda.Closure.Functional.Type-soundness -- A very brief treatment of different kinds of term equivalences, -- including contextual equivalence and applicative bisimilarity. import Lambda.Closure.Equivalences -- A functional semantics, a compiler and a compiler correctness -- proof, and a type soundness proof for a non-deterministic untyped -- λ-calculus with constants. import Lambda.Closure.Functional.Non-deterministic -- A variant of the code above without the workarounds used to -- convince Agda that the code is productive. import Lambda.Closure.Functional.Non-deterministic.No-workarounds