nLab CompLF v1

Contents

Contents

Idea

This is the definition of the formal system CompLF, version 1. Actually, there were several versions between zero and one, but you’re not missing anything interesting.

Syntax

Term grammar

The main syntactic class is terms. Type expressions are terms. There are also variables and contexts.

variables (xx, yy, …) ::= (Written as usual. Complain if you can’t tell them apart from metavariables.)

terms (tt, aa, bb, ff, TT, AA, BB, RR, …) ::=

  • xx \qquad (variable reference)

  • λx.b\lambda x.b \qquad (lambda abstraction)

  • faf\,a \qquad (application)

  • ttt \equiv t' \qquad (identity type) (computational equivalence)

  • a=bCa = b \in C \qquad (equality type)

  • Relax(A)Relax(A) \qquad (“relax” type)

  • Πx:A.B\Pi x:A.B \qquad (dependent function type)

  • x:A.B\cap x:A.B \qquad (family intersection type)

  • {x:A|B}\{x:A | B\} \qquad (subset/separation type)

  • CompComp \qquad (type of computations (realizers))

  • BoolBool \qquad (type of “booleans”) (two-element type)

  • {x=y|R}\{x = y | R\} \qquad (PER comprehension type)

  • NatNat \qquad (type of natural numbers)

contexts (Γ\Gamma, …) ::= \cdot | Γ,x:T\Gamma,x:T

As usual, the rules may make liberal use of informal list operations to work with contexts.

Abbreviations

Semantic Judgment Forms

aAa=aAa \in A\;\coloneqq\;a = a \in A

ABΠ̲:A.BA \to B\;\coloneqq\;\Pi \underline{\;}:A.B

AB̲:A.BA \supset B\;\coloneqq\;\cap \underline{\;}:A.B

AB{̲:A|B}A \wedge B\;\coloneqq\;\{\underline{\;}:A | B\}

Computations

The Church booleans:

truλt.λf.ttru\;\coloneqq\;\lambda t.\lambda f.t

flsλt.λf.ffls\;\coloneqq\;\lambda t.\lambda f.f

Scott nats:

zroλz.λs.zzro\;\coloneqq\;\lambda z.\lambda s.z

suc(n)λz.λs.snsuc(n)\;\coloneqq\;\lambda z.\lambda s.s\,n

Type Constructors

The type constructors given in the grammar above that have subexpressions are actually abbreviations for applied constants. For example:

Πx:A.BKPiA(λx.B)\Pi x:A.B\;\coloneqq\;KPi\,A\,(\lambda x.B)

In particular, λ\lambda is the only real binding form of the language.

tru=truBool\top\;\coloneqq\;tru = tru \in Bool

tru=flsBool\bot\;\coloneqq\;tru = fls \in Bool

Judgment forms

a βba \longrightarrow_\beta b \qquad (beta “reduction”)

ΓTtype\Gamma \vdash T\,type \qquad (type validity)

ΓtT\Gamma \vdash t \Vdash T \qquad (element in a type) (realizer of a type)

Rules

Partially-Compatible Reduction

(λx.b)a βb[a/x] b βbλx.b βλx.b a βafa βfa\begin{gathered} \frac{}{(\lambda x.b)\,a \longrightarrow_\beta b[a/x]} \\ \\ \frac{b \longrightarrow_\beta b'} {\lambda x.b \longrightarrow_\beta \lambda x.b'} \\ \\ \frac{a \longrightarrow_\beta a'} {f\,a \longrightarrow_\beta f\,a'} \end{gathered}

Miscellaneous

x:TΓΓxT A βBΓtAΓtB B βAΓtAΓtB ΓaAΓAtype\begin{gathered} \frac{x:T \in \Gamma}{\Gamma \vdash x \Vdash T} \\ \\ \\ \frac{A \longrightarrow_\beta B \qquad \Gamma \vdash t \Vdash A} {\Gamma \vdash t \Vdash B} \\ \\ \frac{B \longrightarrow_\beta A \qquad \Gamma \vdash t \Vdash A} {\Gamma \vdash t \Vdash B} \\ \\ \\ \frac{\Gamma \vdash a \Vdash A}{\Gamma \vdash A\,type} \end{gathered}

Relax

ΓAtypeΓRelax(A)type ΓRelax(A)typeΓAtype ΓaAΓaRelax(A) ΓAtypeΓtCompΓtRelax(A) ΓaComp Γp1(aA)(a=aA) Γp2(aA)(a=aA)Γqa=aRelax(A) ΓaAΓpa=aRelax(A)Γqa=aA\begin{gathered} \frac{\Gamma \vdash A\,type}{\Gamma \vdash Relax(A)\,type} \\ \\ \frac{\Gamma \vdash Relax(A)\,type}{\Gamma \vdash A\,type} \\ \\ \\ \frac{\Gamma \vdash a \Vdash A}{\Gamma \vdash a \Vdash Relax(A)} \\ \\ \frac{\Gamma \vdash A\,type \qquad \Gamma \vdash t \Vdash Comp} {\Gamma \vdash t \Vdash Relax(A)} \\ \\ \\ \frac{\begin{array}{l}\Gamma \vdash a' \Vdash Comp \\ \Gamma \vdash p1 \Vdash (a \in A) \supset (a = a' \in A) \\ \Gamma \vdash p2 \Vdash (a' \in A) \supset (a = a' \in A)\end{array}} {\Gamma \vdash q \Vdash a = a' \in Relax(A)} \\ \\ \frac{\Gamma \vdash a \Vdash A \qquad \Gamma \vdash p \Vdash a = a' \in Relax(A)} {\Gamma \vdash q \Vdash a = a' \in A} \end{gathered}

Equality

Γa1Relax(A)Γa2Relax(A)Γa1=a2Atype Γa1=a2AtypeΓa1Relax(A)Γa1=a2AtypeΓa2Relax(A) ΓaAΓqp1=p2(a=aA) Γpa=aAΓaA Γpa=aAΓ,x:ACtypeΓcC[a/x]ΓcC[a/x]\begin{gathered} \frac{\Gamma \vdash a1 \Vdash Relax(A) \qquad \Gamma \vdash a2 \Vdash Relax(A)} {\Gamma \vdash a1 = a2 \in A\,type} \\ \\ \frac{\Gamma \vdash a1 = a2 \in A\,type}{\Gamma \vdash a1 \Vdash Relax(A)} \qquad \frac{\Gamma \vdash a1 = a2 \in A\,type}{\Gamma \vdash a2 \Vdash Relax(A)} \\ \\ \\ \frac{\Gamma \vdash a \Vdash A} {\Gamma \vdash q \Vdash p1 = p2 \in (a = a \in A)} \\ \\ \frac{\Gamma \vdash p \Vdash a = a' \in A}{\Gamma \vdash a \Vdash A} \\ \\ \frac{\Gamma \vdash p \Vdash a = a' \in A \qquad \Gamma,x:A \vdash C\,type \qquad \Gamma \vdash c \Vdash C[a/x]} {\Gamma \vdash c \Vdash C[a'/x]} \end{gathered}

Identity

Γt1CompΓt2CompΓt1t2type Γqp1=p2(tt) ΓpttΓcC[t/x]ΓcC[t/x]\begin{gathered} \frac{\Gamma \vdash t1 \Vdash Comp \qquad \Gamma \vdash t2 \Vdash Comp} {\Gamma \vdash t1 \equiv t2\,type} \\ \\ \\ \frac{}{\Gamma \vdash q \Vdash p1 = p2 \in (t \equiv t)} \\ \\ \frac{\Gamma \vdash p \Vdash t \equiv t' \qquad \Gamma \vdash c \Vdash C[t/x]} {\Gamma \vdash c \Vdash C[t'/x]} \end{gathered}

Functions

ΓAtypeΓ,x:ABtypeΓΠx:A.Btype ΓΠx:A.BtypeΓAtype ΓΠx:A.BtypeΓaAΓB[a/x]type ΓfΠx:A.BΓaAΓfaB[a/x] ΓAtypeΓ,x:Apfx=fxBxFV(f,f)Γqf=fΠx:A.B\begin{gathered} \frac{\Gamma \vdash A\,type \qquad \Gamma,x:A \vdash B\,type} {\Gamma \vdash \Pi x:A.B\,type} \\ \\ \frac{\Gamma \vdash \Pi x:A.B\,type}{\Gamma \vdash A\,type} \\ \\ \frac{\Gamma \vdash \Pi x:A.B\,type \qquad \Gamma \vdash a \Vdash A} {\Gamma \vdash B[a/x]\,type} \\ \\ \\ \frac{\Gamma \vdash f \Vdash \Pi x:A.B \qquad \Gamma \vdash a \Vdash A} {\Gamma \vdash f\,a \Vdash B[a/x]} \\ \\ \frac{\Gamma \vdash A\,type \qquad \Gamma,x:A \vdash p \Vdash f\,x = f'\,x \in B \qquad x \notin FV(f,f')} {\Gamma \vdash q \Vdash f = f' \in \Pi x:A.B} \end{gathered}

Intersection

ΓAtypeΓ,x:ABtypeΓx:A.Btype Γx:A.BtypeΓAtype Γx:A.BtypeΓaAΓB[a/x]type Γbx:A.BΓaAΓbB[a/x] ΓAtypeΓ,x:Apb=bBxFV(b,b)Γqb=bx:A.B\begin{gathered} \frac{\Gamma \vdash A\,type \qquad \Gamma,x:A \vdash B\,type} {\Gamma \vdash \cap x:A.B\,type} \\ \\ \frac{\Gamma \vdash \cap x:A.B\,type}{\Gamma \vdash A\,type} \\ \\ \frac{\Gamma \vdash \cap x:A.B\,type \qquad \Gamma \vdash a \Vdash A} {\Gamma \vdash B[a/x]\,type} \\ \\ \\ \frac{\Gamma \vdash b \Vdash \cap x:A.B \qquad \Gamma \vdash a \Vdash A} {\Gamma \vdash b \Vdash B[a/x]} \\ \\ \frac{\Gamma \vdash A\,type \qquad \Gamma,x:A \vdash p \Vdash b = b' \in B \qquad x \notin FV(b,b')} {\Gamma \vdash q \Vdash b = b' \in \cap x:A.B} \end{gathered}

Subset

ΓAtypeΓ,x:ABtypeΓ{x:A|B}type Γ{x:A|B}typeΓAtype Γ{x:A|B}typeΓaAΓB[a/x]type Γ,x:ABtypeΓaAΓbB[a/x]Γa{x:A|B} Γa{x:A|B}Γ,x:A,y:BcCyFV(c,C)Γc[a/x]C[a/x]\begin{gathered} \frac{\Gamma \vdash A\,type \qquad \Gamma,x:A \vdash B\,type} {\Gamma \vdash \{x:A | B\}\,type} \\ \\ \frac{\Gamma \vdash \{x:A | B\}\,type}{\Gamma \vdash A\,type} \\ \\ \frac{\Gamma \vdash \{x:A | B\}\,type \qquad \Gamma \vdash a \Vdash A} {\Gamma \vdash B[a/x]\,type} \\ \\ \\ \frac{\Gamma,x:A \vdash B\,type \qquad \Gamma \vdash a \Vdash A \qquad \Gamma \vdash b \Vdash B[a/x]} {\Gamma \vdash a \Vdash \{x:A | B\}} \\ \\ \frac{\Gamma \vdash a \Vdash \{x:A | B\} \qquad \Gamma,x:A,y:B \vdash c \Vdash C \qquad y \notin FV(c,C)} {\Gamma \vdash c[a/x] \Vdash C[a/x]} \end{gathered}

Computations

ΓComptype Γ,x:CompbCompΓλx.bComp ΓfCompΓaCompΓfaComp ΓaAΓ,y:ACtype Γ,x:Comp,x:Comp,h:(x=xA)pc[x/y]=c[x/y]C[x/y] x,x,hFV(c,c)Γqc[a/y]=c[a/y]C[a/y]\begin{gathered} \frac{}{\Gamma \vdash Comp\,type} \\ \\ \\ \frac{\Gamma,x:Comp \vdash b \Vdash Comp}{\Gamma \vdash \lambda x.b \Vdash Comp} \\ \\ \frac{\Gamma \vdash f \Vdash Comp \qquad \Gamma \vdash a \Vdash Comp} {\Gamma \vdash f\,a \Vdash Comp} \\ \\ \\ \frac{\begin{array}{l}\Gamma \vdash a \Vdash A \qquad \Gamma,y:A \vdash C\,type \\ \Gamma,x:Comp,x':Comp,h:(x = x' \in A) \vdash p \Vdash c[x/y] = c'[x'/y] \in C[x/y] \\ x,x',h \notin FV(c,c')\end{array}} {\Gamma \vdash q \Vdash c[a/y] = c'[a/y] \in C[a/y]} \end{gathered}

Booleans

ΓBooltype ΓtruBoolΓflsBool ΓbBoolΓcC[tru/x]ΓcC[fls/x]ΓcC[b/x]\begin{gathered} \frac{}{\Gamma \vdash Bool\,type} \\ \\ \frac{}{\Gamma \vdash tru \Vdash Bool} \qquad \frac{}{\Gamma \vdash fls \Vdash Bool} \\ \\ \frac{\Gamma \vdash b \Vdash Bool \qquad \Gamma \vdash c \Vdash C[tru/x] \qquad \Gamma \vdash c \Vdash C[fls/x]} {\Gamma \vdash c \Vdash C[b/x]} \end{gathered}

PER

Γ,x1:Comp,x2:CompRtype Γ,y1:Comp,y2:CompsR[y1,y2/x1,x2]R[y2,y1/x1,x2] Γ,y1:Comp,y2:Comp,y3:ComptR[y1,y2/x1,x2]R[y2,y3/x1,x2]R[y1,y3/x1,x2]Γ{x1=x2|R}type Γ{x1=x2|R}typeΓt2CompΓpR[t1,t2/x1,x2]Γqt1=t2{x1=x2|R} Γpt1=t2{x1=x2|R} ΓR[t1,t2/x1,x2]type Γ,h:R[t1,t2/x1,x2]cChFV(c,C)ΓcC\begin{gathered} \frac{\begin{array}{l}\Gamma,x1:Comp,x2:Comp \vdash R\,type \\ \Gamma,y1:Comp,y2:Comp \vdash s \Vdash R[y1,y2/x1,x2] \supset R[y2,y1/x1,x2] \\ \Gamma,y1:Comp,y2:Comp,y3:Comp \vdash t \Vdash R[y1,y2/x1,x2] \supset R[y2,y3/x1,x2] \supset R[y1,y3/x1,x2]\end{array}} {\Gamma \vdash \{x1 = x2 | R\}\,type} \\ \\ \\ \frac{\Gamma \vdash \{x1 = x2 | R\}\,type \qquad \Gamma \vdash t2 \Vdash Comp \qquad \Gamma \vdash p \Vdash R[t1,t2/x1,x2]} {\Gamma \vdash q \Vdash t1 = t2 \in \{x1 = x2 | R\}} \\ \\ \frac{\begin{array}{l} \Gamma \vdash p \Vdash t1 = t2 \in \{x1 = x2 | R\} \\ \Gamma \vdash R[t1,t2/x1,x2]\,type \\ \Gamma,h:R[t1,t2/x1,x2] \vdash c \Vdash C \qquad h \notin FV(c,C) \end{array}} {\Gamma \vdash c \Vdash C} \end{gathered}

Natural Numbers

ΓNattype ΓzroNat ΓnNatΓsuc(n)Nat ΓnNatΓnComp ΓnNatΓ,x:NatCtype ΓcC[zro/x] Γ,x:Nat,h:CcC[suc(x)/x]ΓcC[n/x]\begin{gathered} \frac{}{\Gamma \vdash Nat\,type} \\ \\ \\ \frac{}{\Gamma \vdash zro \Vdash Nat} \\ \\ \frac{\Gamma \vdash n \Vdash Nat}{\Gamma \vdash suc(n) \Vdash Nat} \\ \\ \\ \frac{\Gamma \vdash n \Vdash Nat}{\Gamma \vdash n \Vdash Comp} \\ \\ \frac{\begin{array}{l} \Gamma \vdash n \Vdash Nat \qquad \Gamma,x:Nat \vdash C\,type \\ \Gamma \vdash c \Vdash C[zro/x] \\ \Gamma,x:Nat,h:C \vdash c \Vdash C[suc(x)/x] \end{array}} {\Gamma \vdash c \Vdash C[n/x]} \end{gathered}

Last revised on July 17, 2020 at 22:33:36. See the history of this page for a list of all contributions to it.