------------------------------------------------------------------------ -- Formalisation of subtyping for recursive types -- -- Nils Anders Danielsson ------------------------------------------------------------------------ -- Partly based on "Coinductive Axiomatization of Recursive Type -- Equality and Subtyping" by Michael Brandt and Fritz Henglein. module RecursiveTypes where -- Recursive types and potentially infinite trees. import RecursiveTypes.Syntax -- Substitutions. import RecursiveTypes.Substitution -- The semantics of recursive types, defined in terms of the trees -- that you get when unfolding them. import RecursiveTypes.Semantics -- The definition of subtyping which, in my eyes, is the most obvious. -- Some people may dislike coinductive definitions, though. import RecursiveTypes.Subtyping.Semantic.Coinductive -- Another definition of subtyping, this time in terms of finite -- approximations. According to Brandt and Henglein this definition is -- due to Amadio and Cardelli. import RecursiveTypes.Subtyping.Semantic.Inductive -- The two semantical definitions of subtyping above can easily be -- proved equivalent. import RecursiveTypes.Subtyping.Semantic.Equivalence -- An axiomatisation of subtyping which is inspired by Brandt and -- Henglein's. The main difference is that their axiomatisation is -- inductive, using explicit hypotheses to get a coinductive flavour, -- whereas mine is mixed inductive/coinductive, using no explicit -- hypotheses. The axiomatisation is proved equivalent to the -- coinductive semantic definition of subtyping. The proof is a lot -- simpler than Brandt and Henglein's, but their proof includes a -- decision procedure for subtyping. import RecursiveTypes.Subtyping.Axiomatic.Coinductive -- Brandt and Henglein's axiomatisation, plus some proofs: -- • A proof showing that the axiomatisation is sound with respect to -- the ones above. The soundness proof is different from the one -- given by Brandt and Henglein: it is cyclic (but productive). -- • Proofs of decidability and completeness, based on Brandt and -- Henglein's algorithm. import RecursiveTypes.Subtyping.Axiomatic.Inductive -- Some modules containing supporting code for the proof of -- decidability, including Brandt and Henglein's subterm relation. import RecursiveTypes.Subterm import RecursiveTypes.Subterm.RestrictedHypothesis import RecursiveTypes.Syntax.UnfoldedOrFixpoint