------------------------------------------------------------------------ -- A definition of a big-step semantics which handles termination and -- non-termination at the same time, without duplication of rules ------------------------------------------------------------------------ module Lambda where -- Syntax of an untyped λ-calculus. import Lambda.Syntax -- 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.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.TwoSemantics -- The two definitions are equivalent. import Lambda.Equivalence -- A formulation of the semantics which uses closures and -- environments. Leroy and Grall define a similar semantics but split -- it up into several definitions, like in TwoSemantics above. import Lambda.Closure -- A virtual machine, a compiler from the λ-calculus defined above -- into the language of the virtual machine, and a proof showing that -- the compiler preserves the semantics defined in Lambda.Closure -- (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.VirtualMachine