~aathn/kalpis-agda

A complete Agda formalization of the Kalpis programming language
Apply Kick-the-tires feedback
6e828ff3 — Kazutaka Matsuda 6 months ago
I think it can typecheck under Agda 2.7.3/standard-library 1.7.1

refs

master
browse  log 

clone

read-only
https://git.sr.ht/~aathn/kalpis-agda
read/write
git@git.sr.ht:~aathn/kalpis-agda

You can also use your local clone with git send-email.

#Agda formalization of the languages Kalpis and RRArr

This repository contains an Agda formalization of the semantics of Kalpis and RRArr, presented in the ESOP24 paper Reconciling Partial and Local Invertibility (Ågren Thuné, Matsuda and Wang 2024). The main purpose of this implementation is to be type-checked, rather than to be executed.

#Prerequisites

The code in this repository was tested using Agda versions 2.6.3/2.6.4 and Agda stdlib version 1.7.1/1.7.3. Your mileage may vary on other versions (but we suspect that any sufficiently recent version supporting sized types should work).

#Type Checking the Proofs

To type check the proofs, invoke make at the project root, or manually run agda Everything.agda. Agda will then type check all modules of the repository, outputting a line Checking ... for each one to indicate its progress.

Note that this will take a long time (up to an hour or more), with the vast majority of the time spent on the file Kalpis/Properties/Completeness.agda. To reduce the type-checking time (if you trust us), you can disable the termination checker for that file by uncommenting the line {-# OPTIONS --no-termination-check #-} at the top of the file. With this line uncommented, the type-checking finishes in roughly 10 minutes on the development machine.

Type checking the proofs produces cache files in the _build folder, which makes consecutive executions faster. If you wish to remove the cache files to check the proofs from scratch, run make clean, or simply remove the _build folder.

#Correspondence to the Paper

This mechanized development is mentioned as a contribution in Section 1.1 of the paper. Thus, we have strived to keep definitions and proofs here very close to the paper's presentation, but there are a few differences.

  • This Agda formalization uses a well-scoped and intrinsically typed syntax based on De Bruijn indices, both for terms and types.

  • The dynamic semantics of Sections 3.5 and 4.2 in the paper are implemented in the form of definitional interpreters, using the sized delay monad to allow nontermination.

  • We use different arrow symbols to the paper's notation---double arrows for arrow combinator types and squiggly arrows for higher-order function types (see the table below).

  • For Theorems 3 and 4 in the paper, the Agda code features only the full version of the proof which covers the higher-order constructs introduced in Section 4.5 in the paper. Hence, the statements of these theorems are slightly more complicated than in the paper, and more resemble the paper's Theorems 5 and 6.

  • As stated in Section 5 of the paper, we fix the set of datatype constructors to tunit, _⊗_, _⊕_, and μ A (in addition to functional types) without loss of generality.

  • We do not implement the invertible first-match policy, instead observing only the first postcondition of a binary match (_⊕_) and ignoring the postcondition for unary matches (tunit, _⊗_, and μ A).

#Proof Methodology

All major proofs are performed by well-founded induction on the step-count of evaluation, using the machinery in agda-stdlib's Data.Nat.Induction. More precisely, the 'step count' is the number of later constructors (of the delay monad) wrapping the computation, and we use a judgment n ⊢ d ↠ v (defined in PInj.agda) to denote d evaluating to v in a finite n number of steps. To denote a pair of partial functions we use the notation i ⊢ A ⇔ B (defined in PInj.agda), where i is the Size of the results. The property IsPInj (n : ℕ) (f : ∞ ⊢ A ⇔ B) (defined in PInj.agda) then asserts that n-step evaluation of f has an n-step inverse in each direction. By proving this property for all n, we can show that f is a partial injection such that forward and backward evaluation always take the same number of steps.

For semantics preservation proofs, we typically have to prove multiple mutually recursive statements for each of the soundness and completeness statements: one for unidirectional terms and one or two for invertible terms. We use a naming convention where the soundness theorem is called LangA⊇LangB (e.g., Kalpis⊇RRArr), and the completeness theorem is called LangB⊇LangA (e.g., RRArr⊇Kalpis) for a translation from LangA to LangB. Each 'helper statement' is named Aterm⊇Bterm, where Aterm and Bterm are the Agda names/notations for the corresponding terms (e.g., UTerm⊇⇒ for Kalpis and RRArr unidirectional terms).

#Usage of Sized Types

This development uses Agda's Sized Types (--sized-types) to allow modelling non-termination in our definitional interpreters. Although this flag is known to be unsound in general, we use it only through modules defined in Agda's standard library (Codata.Delay and Codata.Thunk) which we believe to be sound. In addition, we use them only in a limited set of our own modules, namely the ones defining and reasoning about the definitional interpreters for each language (PInj.adga, PiArr/{Definitional,Properties}.agda, RRArr/{Definitional,Properties}.agda, Kalpis/{Definitional,Properties/*}.agda). Although these modules together constitute a significant number of lines of code, we hope that it should be clear that no intentional abuse of --sized-types is performed in them.

#Paper-to-Artifact Correspondence Guide

The table below enumerates the definitions and theorems stated in the paper and lists the corresponding Agda definitions in this mechanization. For each definition, the relevant language is stated first: Kalpis/RRArr/PiArr, where PiArr is our variant of Πᵒ with higher-order constructs. Then, the definition / theorem and its location in the paper is given, after which location and name of the corresponding Agda definition(s) follow. For the last column, helper functions or cases to note are sometimes given in parentheses after the main definition(s).

Language Definition / Theorem Paper File Agda definition
Kalpis Unidirectional term syntax Page 9 Kalpis/Syntax.agda UTerm
Kalpis Invertible term syntax Page 9 Kalpis/Syntax.agda RTerm
Kalpis Constructor/pattern syntax Page 9 Kalpis/Syntax.agda Con
Kalpis Datatype constructor syntax Page 10 Kalpis/Types.agda TyCon
Kalpis Type syntax Page 10 Kalpis/Types.agda Ty
Kalpis Unidirectional term typing Page 12, Fig. 1 Kalpis/Syntax.agda UTerm
Kalpis Invertible term typing Page 12, Fig. 1 Kalpis/Syntax.agda RTerm
Kalpis Pattern typing Page 12, Fig. 1 Kalpis/Syntax.agda Con
Kalpis Values Page 13 Kalpis/Value.agda Value
Kalpis Value environments Page 13 Kalpis/Value.agda ValEnv
Kalpis Unidirectional evaluation Page 14, Fig. 2 Kalpis/Definitional.agda evalU
Kalpis Forward/backward evaluation Page 14, Fig. 2 Kalpis/Definitional.agda evalR
Kalpis Theorem 1 (Subject reduction) Page 14 Kalpis/Definitional.agda evalU, evalR
Kalpis Theorem 2 (Invertibility) Page 15 Kalpis/Properties/Invertibility.agda evalR-pinj (evalR-pinj-ind)
RRArr Unidirectional arrow syntax and typing Page 16, Fig. 3 RRArr/Syntax.agda _⇒_
RRArr Invertible arrow syntax and typing Page 16, Fig. 3 RRArr/Syntax.agda _·_⇔_
RRArr Base invertible combinators Page 16, Fig. 3 RRArr/PiO/Syntax.agda _⇔_
RRArr Values Page 17 RRArr/Value.agda Value
RRArr Unidirectional evaluation Page 18, Fig. 4 RRArr/Definitional.agda evalU
RRArr Forward/backward evaluation Page 18, Fig. 4 RRArr/Definitional.agda evalR
RRArr Subject reduction Page 17 RRArr/Definitional.agda evalU, evalR
RRArr Invertibility Page 17 RRArr/Properties.agda ·⇔-pinj (·⇔-pinj-ind)
PiArr Syntax of Πᵒ Page 17, Fig. 5 PiArr/Syntax.agda _⇔_
RRArr/PiArr Translation to Πᵒ (unidirectional arrows) Pages 17-20 RRArr/ToPiArr.agda ⟦_⟧⇒
RRArr/PiArr Translation to Πᵒ (invertible arrows) Pages 17-20 RRArr/ToPiArr.agda ⟦_⟧·
RRArr/PiArr Theorem 3 (RRArr-->Πᵒ soundness) Page 20 RRArr/Properties.agda RRArr⊇PiArr (⇒⊇⇔ᵃ, ·⇔⊇⇔ᵃ)
RRArr/PiArr Theorem 4 (RRArr-->Πᵒ completeness) Page 20 RRArr/Properties.agda PiArr⊇RRArr (⇔ᵃ⊇⇒, ⇔ᵃ⊇·⇔-fwd, ⇔ᵃ⊇·⇔-bwd)
RRArr Higher-order combinator syntax and typing Page 20, Fig. 6 RRArr/Syntax.agda _⇒_, _·_⇔_ (curry, curry●, app, app●)
RRArr Higher-order combinator semantics Page 20, Fig. 6 RRArr/Definitional.agda evalU, evalR (curry, curry●, app, app●)
PiArr Higher-order combinator syntax Page 21 PiArr/Syntax.agda _⇔_ (curry, app)
PiArr Higher-order combinator semantics Page 21 PiArr/Definitional.agda eval (curry, app)
RRArr/PiArr Translation of higher-order combinators Page 21 RRArr/ToPiArr.agda ⟦_⟧⇒, ⟦_⟧· (curry, curry●, app, app●)
RRArr/PiArr Theorems 3,4 with higher-order combinators Page 21 RRArr/Properties.agda RRArr⊇PiArr, PiArr⊇RRArr (curry, curry●, app, app●)
Kalpis/RRArr Γˣ operation Page 22 Kalpis/ToRRArr.agda ⟦_⟧ˣ
Kalpis/RRArr lookupₓ combinator Page 22 Kalpis/ToRRArr.agda lookupVar
Kalpis/RRArr splitΘ₁,Θ₂ combinator Page 22 Kalpis/ToRRArr.agda splitEnv
PiArr distl combinator Page 22 PiArr/Syntax.agda distl (we take this as the primitive and derive distr)
RRArr case combinator Page 22 RRArr/Syntax.agda caseᵣ
RRArr mkCond operator Page 22 Kalpis/ToRRArr.agda case●-postcond
Kalpis/RRArr Translation to RRArr (unidirectional terms) Pages 21-23 Kalpis/ToRRArr.agda ⟦_⟧ᵘ
Kalpis/RRArr Translation to RRArr (invertible terms) Pages 21-23 Kalpis/ToRRArr.agda ⟦_⟧ʳ
Kalpis/RRArr Translation to RRArr (values and environments) Page 23 Kalpis/ToRRArr.agda ⟦_⟧ᵛ, ⟦_⟧ᵉ
Kalpis/RRArr Theorem 5 (Kalpis-->RRArr soundness) Page 23 Kalpis/Properties/Soundness.agda Kalpis⊇RRArr (UTerm⊇⇒, RTerm⊇·⇔)
Kalpis/RRArr Theorem 6 (Kalpis-->RRArr completeness) Page 23 Kalpis/Properties/Completeness.agda RRArr⊇Kalpis (⇒⊇UTerm, ·⇔⊇RTerm-fwd, ·⇔⊇RTerm-bwd)

#Repository Structure

The repository is structured into folders based on the various languages formalized (Kalpis/, RRArr/, and PiArr/, where PiArr is Πᵒ extended with higher-order constructs). Each folder contains at least Syntax.agda defining the language's intrinsically typed syntax, Definitional.agda giving a definitional interpreter of the language, and Properties.agda establishing properties like invertibility of the corresponding semantics. For an overview of all modules, see Everything.agda at the repository root, which also provides more detailed descriptions of each module's contents.