Formal Metatheory of Second-Order Abstract Syntax

• Preprint
• Virtual machine
• Browsable source code
• Browsable examples
• GitHub repository

Instructions

1. If building from source, clone the Git repository (and submodules) with git clone --recurse-submodules https://github.com/DimaSamoz/agda-soas.git.
2. If using VirtualBox:
   1. Download the virtual machine and double-click on the downloaded SOAS.ova file (or File > Import Appliance... in VirtualBox).
   2. Launch the virtual machine with VirtualBox and log in with username agda-soas and password popl2022-agda-soas. You may need to resize the window or tweak the Display settings in VirtualBox to adjust scaling.
   3. Open Emacs and navigate to the ~/agda-soas directory (or navigate to ~/agda-soas in the Terminal and open Emacs with emacs .)
3. Open any of the code files in the SOAS directory (the modules are listed in Everything.agda) and load it with C-c C-l. Same for example files, found in the subfolders of the out directory.
4. Call the code generation script with python3 soas.py <filename>, with some examples given in the gen/ex directory.

Correspondence guide

Much of the code in the library is directly included in the paper. Below is a section-by-section listing of the defined concepts and their location in the source code.

The formalisation depends on the Agda standard library and category theory library, and uses implicit and explicit function extensionality (and some derived properties for convenience). The REWRITE pragma is used for some nonessential proofs that are not required for the main results.

2. Mathematical foundations

Formalisation of abstract mathematical concepts used in the library, including the standard inductive definition of contexts and variables (typed de Bruijn indices), type- and context-indexed families of sets, the axiomatisation of renaming and substitution structure, and properties of functions that incorporate a substitution.

2.1. Contexts and families

• Definitions of contexts, variables, and families.
• Bicartesian closed, and linear monoidal structure of families.
• Context extension endofunctor.
• Context maps and renamings, and their combinators.
• Inductive context maps.
• The cocartesian category of renamings.

2.2. Renaming and substitution

• Box modality, renaming coalgebra and pointed coalgebra structure.
• Examples of coalgebras and homorphisms.
• Internal hom of families and skew-closed structure.
• Substitution monoids and their homomorphisms.

2.3. Parametrised maps

• Coalgebraic maps.
• Coalgebraic strength and lifting as its instance for context extension.
• Derived lifting lemmas.
• Coalgebraic monoids.

3. Initial algebra semantics

The initial algebra semantics approach underlies most of the metatheoretic results. The signature-generic development is accomplished by parametrising the relevant modules with a metavariable family and a signature endofunctor with a coalgebraic strength, and furthermore assuming the existence of an initial meta-algebra for the endofunctor from which initial interpretations can be extracted. Specifically, initiality states that given any meta-algebra 𝒜, there exists a unique meta-algebra homomorphism 𝕤𝕖𝕞 : 𝕋 ⇾ 𝒜 where 𝕋 is the initial meta-algebra assumed to exist.

3.1. Signature algebras and monoids

• Signature algebras with (meta)variables and their homomorphisms. For a signature endofunctor ⅀ and a family of metavariables 𝔛, a (⅀, 𝔛)-meta-algebra (𝒜, 𝑎𝑙𝑔, 𝑣𝑎𝑟, 𝑚𝑣𝑎𝑟) is a carrier family with structure maps for operators, variables, and metavariables.
• Signature monoids and their homomorphisms.

3.3. Parametrised interpretations

• Initial algebra semantics: for a family of metavariables 𝔛, the initial (⅀, 𝔛)-meta-algebra 𝕋 𝔛 can be uniquely interpreted in any meta-algebra.
• Traversals: interpretations into meta-algebras parametrised by a pointed □-coalgebra.
• Lemma 3.2: meta-algebras parametrised by a pointed coalgebra are meta-algebras.
  • Corollary: box modality lifts to meta-algebras.

3.4. ⅀-monoid structure by initiality

• Lemma 3.3: sufficient condition for equality of maps out of initial algebra.
  • Corollaries: equality of maps with one or two parameters.
• Unit traversal theorem: traversal into a meta-algebra with the point of a pointed coalgebra is equivalent to direct interpretation in the meta-algebra.
• Renaming structure by initiality.
  • Counit law corollary of the unit traversal theorem above.
  • Comultiplication law via Lemma 3.3 and strength properties.
• Coalgebraic interpretation maps.
  • Lemma: interpretation is a □-coalgebra homomorphism, as long as the target meta-algebra has compatible □-coalgebra structure.
  • Lemma: traversals commute with renaming, assuming the target meta-algebra has compatible □-coalgebra structure.
  • Coalgebraic traversal map theorem: traversal maps into meta-algebras with compatible □-coalgebra structure are coalgebraic.
• Substitution structure by initiality.
  • Lemma: substitution map is coalgebraic by coalgebraic traversal map theorem above.
  • Unit law and compatibility are corollaries of the unit traversal theorem above.
  • Associativity law via Lemma 3.3, strength properties, and the fact that substitution map is coalgebraic.

3.5. Free ⅀-monoid structure

• Theorem: initial meta-algebra 𝕋 𝔛 over any family of metavariables 𝔛 is a ⅀-monoid.
• Theorem: initial algebra functor 𝕋 is the free ⅀-monoid on families.
  • Lemma: a ⅀-monoid ℳ with mapping 𝔛 ⇾ M is a (⅀, 𝔛)-meta-algebra.
  • Corollary: the induced extension 𝕋 𝔛 ⇾ M is a ⅀-monoid homomorphism.

3.6-7. Metasubstitution and equational systems

• Ground metasubstitution: derived from free ⅀-monoid monad.
• Cartesian exponential strength.
• Enriched metasubstitution derived by initiality.
• Inductive metasubstitution mappings and their interpretation as linear maps of families.
• Signature-generic equational logic that relies on various forms of metasubstitution.
  • Congruence: applying an equality to a subexpression.
  • Axiom: applying an equational axiom scheme to a concrete term.
  • Theorem: applying a theorem (scheme) to a concrete term.

4. Generic signatures

The signature endofunctor forms the brigde between a second-order signature and the generic metatheory. Initial algebras for the endofunctor (i.e. algebraic data types whose constructors form term of the syntax) can be defined in several ways: either by directly using the signature endofunctor and combining every operator into a single constructor, or separating the operators into individual constructors. The latter is more convenient in practice, and there is a Python script that generates the required boilerplate automatically.

4.1-2. Binding signatures and endofunctor

• Second-order binding signatures.
• Inductive argument lists.
• Signature endofunctor and its strength instances.

4.3. Term syntax

• Implicit inductive term encoding
• Example explicit term encoding

4.4. Code generation

• Python code for parsing and code generation: entry script, types, terms, equations.
• Example syntax description files: algebraic structures, logic, computational calculi, miscellaneous.
• Generated Agda files.