diff --git a/plutus-metatheory/README.md b/plutus-metatheory/README.md index 5bc3d1bff22..342cac6707c 100644 --- a/plutus-metatheory/README.md +++ b/plutus-metatheory/README.md @@ -100,234 +100,5 @@ $ jekyll build -s html -d html/_site ## Detailed Description -See the [table of contents](https://plutus.cardano.intersectmbo.org/metatheory/) for an explanation of the structure of the formalisation and links to the code. +See the [Literate Agda Documentation](https://plutus.cardano.intersectmbo.org/metatheory/) for an explanation of the structure of the formalisation and links to the code. -**The below information is deprecated and is in the process of being -replaced by the table of contents document.** - -## Structure of the intrinsically typed formalisation - -The intrinsic formalisation is split into three sections. Firstly, - -1. Types. - -Then, two different implementations of the term language: - -2. Terms indexed by syntactic types (declarative); -3. Terms indexed by normal types (algorithmic). - -## Types - -Types are defined in the -[Type](https://plutus.cardano.intersectmbo.org/metatheory/Type.html) -module. They are intrinsically kinded so it is impossible to apply a -type operator to arguments of the wrong kind. - -The type module is further subdivided into submodules: - -1. [Type.RenamingSubstitution](https://plutus.cardano.intersectmbo.org/metatheory/Type.RenamingSubstitution.html) -contains the operations of renaming and substitution for types and -their proofs of correctness. These are necessary to, for example, -define the beta rule for types in the equational theory and reduction -relation (described below). - -2. [Type.Equality](https://plutus.cardano.intersectmbo.org/metatheory/Type.Equality.html) contains the beta-equational -theory of types. This is essentially a specification for the -computational behaviour of types. - -3. [Type.Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Type.Reduction.html) contains the small step -reduction relation, the progress/preservation results for types, and -an evaluator for types. This result is not used later in the -development but is in the spec. - -4. [Type.BetaNormal](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNormal.html) contains beta normal forms -for types as a separate syntax. Beta normal forms contain no -beta-redexes and guaranteed not to compute any further. - -5. [Type.BetaNBE](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.html) contains a beta normaliser for -types, it is defined in the style of "normalization-by-evaluation" -(NBE) and is guaranteed to terminate. Further submodules define the -correctness proofs for the normalizer and associated operations. - - 1. [Type.BetaNBE.Soundness](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.Soundness.html) contains a - proof that normalizer preserves the meaning of the types. Formally it - states that if we normalize a type then the resultant normal form is - equal (in the equational theory) to the type we started with. - - 2. [Type.BetaNBE.Completeness](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.Completeness.html) - contains a proof that the if we were to normalize two types that are - equal in the equation theory then we will end up with identical normal - forms. - - 3. [Type.BetaNBE.Stability](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.Stability.html) contains a - proof that normalization will preserve syntactic structure of terms - already in normal form. - - 4. [Type.BetaNBE.RenamingSubsitution](https://plutus.cardano.intersectmbo.org/metatheory/Type.BetaNBE.RenamingSubstitution.html) - contains a version of substitution that works on normal forms and - ensures that the result is in normal form. This works by embedding - normal forms back into syntax, performing a syntactic substitution and - then renormalizing. The file also contains a correctness proof for - this version of substitution. - -Note: Crucially, this development of NBE (and anything else in the -formalisation for that matter) does not rely on any postulates -(axioms). Despite the fact that we need to reason about functions in -several places we do not require appealing to function extensionality -which currently requires a postulate in Agda. In this formalisation -the (object) type level programs and their proofs appear in (object) -terms. Appealing to a postulate in type level proofs would stop term -level programs computing. - -## Builtins - -There are builtin types of integers and bytestrings. - -1. [Builtin.Constant.Type](https://plutus.cardano.intersectmbo.org/metatheory/Builtin.Constant.Type.html) -contains the enumeration of the type constants. -2. [Builtin.Constant.Term](https://plutus.cardano.intersectmbo.org/metatheory/Builtin.Constant.Term.html) -contains the enumeration of the term constants at the bottom. -3. [Builtin.Signature](https://plutus.cardano.intersectmbo.org/metatheory/Builtin.Signature.html) -contains the list of builtin operations and their type signatures. In -the specification this information is contained in the large builtin -table. - -The rest of the Builtin machinery: telescopes, and the semantics of -builtins are contained in -[Declarative.Term.Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Term.Reduction.html). - -## Terms indexed by syntactic types - -This is the standard presentation of the typing rules that one may -find in a text book. We can define the terms easily in this style but -using them in further programs/proofs is complicated by the presence -of a separate syntactic constructor for type conversion (type -cast/coercion). The typing rules are not syntax directed which means -it is not possible to directly write a typechecker for these rules as -their is always a choice of rules to apply when building a -derivation. Hence we refer to this version as declarative rather than -algorithmic. In this formalisation where conversion is a constructor -of the syntax not just a typing rule this also affects computation as -we don't know how to process conversions when evaluating. In this -version progress, and evaluation do not handle the conversion -constructor. They fail if they encounter it. Nevertheless this is -sufficient to handle examples which do not require computing the types -before applying beta-reductions. Such as Church/Scott Numerals. - -1. The [Declarative.Term](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Term.html) -module contains the definition of terms. This module has two further submodules: - - 1. [Declarative.Term.RenamingSubstitution](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Term.RenamingSubstitution.html) - contains the definitions of substitution for terms that is necessary to - specify the beta-rules in the reduction relation. This definition and - those it depends on, in turn, depend on the definitions and correctness - proofs of the corresponding type level operations. - - 2. [Declarative.Term.Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Term.Reduction.html) - This file contains the reduction relation for terms (also known - as the small step operational semantics) and the progress proof. - Preservation is inherent. Note: this version of - progress doesn't handle type conversions in terms. - -2. [Declarative.Evaluation](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Evaluation.html) -contains the evaluator the terms. It takes a *gas* argument which is -the number of steps of reduction that are allowed. It returns both a -result and trace of reduction steps or *out of gas*. Note: this -version of evaluation doesn't handle type conversions in terms. - -3. [Declarative.Examples](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Examples.html) -contains some examples of Church and Scott Numerals. Currently it is -very memory intensive to type check this file and/or run examples. - -4. [Erasure](https://plutus.cardano.intersectmbo.org/metatheory/Declarative.Erasure.html) - -## Terms indexed by normal types - -This version is able to handle type conversion by using the normalizer -described above to ensure that types are always in normal form. This -means that no conversion constructor is necessary as any two types -which one could convert between are already in identical normal -form. Here the typing rules are syntax directed and we don't have to -deal with conversions in the syntax. This allows us to define -progress, preservation, and evaluation for the full language of System -F omega with iso-recursive types and sized integers and bytestrings. - -1. The [Algorithmic.Term](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Term.html) -module contains the definition of terms. This module has two further submodules: - - 1. [Algorithmic.Term.RenamingSubstitution](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Term.RenamingSubstitution.html) - contains the definitions of substitution for terms that is - necessary to specify the beta-rules in the reduction - relation. This definition and those it depends on, in turn, - depend on the definitions and correctness proofs of the - corresponding type level operations. In this version this - includes depeneding on the correctness proof of the beta - normalizer for types. - - 2. [Algorithmic.Term.Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Term.Reduction.html) - This file contains the reduction relation for terms (also known - as the small step operational semantics) and the progress proof. - Preservation is, again, inherent. - -2. [Algorithmic.Evaluation](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Evaluation.html) -contains the evaluator the terms. It takes a *gas* argument which is -the number of steps of reduction that are allowed. It returns both a -result and trace of reduction steps or *out of gas*. - -3. [Algorithmic.Examples](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Examples.html) -contains some examples of Church and Scott Numerals. Currently it is -very memory intensive to type check this file and/or run examples. - -We also need to show that the algorithmic version of the type system is sound and complete. - -4. [Algorithmic.Soundness](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Soundness.html) - -Programmatically this corresponds to taking a term with normal type -and converting it back to a term with a syntactic type. This -introduces conversions into the term anywhere there a substitution -occurs in a type. - -4. [Algorithmic.Completeness](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Completeness.html) - -5. [Erasure](https://plutus.cardano.intersectmbo.org/metatheory/Algorithmic.Erasure.html) contains erasure to untyped lambda calculus. - -Programmatically this correponds to taking a term with a syntactic -type that may contain conversions and normalising its type by -collapsing all the conversions. - -# Extrinsically typed version - -1. [Syntax](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.html) -contains the intrinsically scoped but extrinsically typed terms, and -intrinsically scoped but extrinscically kinded types. - -2. [Renaming and -Substitution](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.RenamingSubstitution.html) -contains the operations of renaming and substitution for extrinsically -typed terms, and extrinsically kinded types. - -3. [Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.Reduction.html) contains the reduction rules, progress and evaluation. - -4. [Extrication](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.Extrication.html) -contains the operations to convert from intrinsically typed to -extrinscally typed syntax. - -5. [Erasure](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.Erasure.html) -contains operations to erase the types yielding untyped terms. - - 1. [Renaming and - Substitution](https://plutus.cardano.intersectmbo.org/metatheory/Scoped.Erasure.RenamingSubstitution.html) - contains operations to erase the types in extrinsic renamings and - substitutions yielding untyped renamings and substitutions. - -# Untyped version - -1. [Syntax](https://plutus.cardano.intersectmbo.org/metatheory/Untyped.html) -contains intrinsically scoped but untyped lambda calculus extended -with builtins. - -2. [Renaming and -Substitution](https://plutus.cardano.intersectmbo.org/metatheory/Untyped.RenamingSubstitution.html) -contains operations for untyped renaming and substitution. - -3. [Reduction](https://plutus.cardano.intersectmbo.org/metatheory/Untyped.Reduction.html) contains the untyped reduction rules.