Chuangjie Xu 2013 (updated and ported to TypeTopology in 2025)

This module collects the bare syntax of GΓΆdel's System T used throughout the
C-space development.

It is intentionally syntax-only: there are no reduction rules, typing
judgements, or semantic interpretations here. Those belong in the modules that
use the language.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module C-Spaces.Syntax.SystemT where

open import MLTT.Spartan

\end{code}

Types

The simple types of System T are generated from booleans, natural numbers,
binary products, and function spaces.

\begin{code}

infixr 10 _⊠_
infixr 10 _⇨_

data Ty : 𝓀₀ Μ‡  where
 β‘‘ : Ty
 Ⓝ : Ty
 _⊠_ : Ty β†’ Ty β†’ Ty
 _⇨_ : Ty β†’ Ty β†’ Ty

\end{code}

Contexts and variables

Contexts are represented as snoc-lists. The operation `Ξ“ β‚Š Οƒ` extends the
context `Ξ“` with a fresh variable of type `Οƒ`.

Variables are represented by de Bruijn indices. Since the context is a
snoc-list, `zero` refers to the most recently added variable and `succ`
steps to the left in the context.

\begin{code}

infixl 10 _β‚Š_

data Cxt : 𝓀₀ Μ‡  where
 Ξ΅ : Cxt
 _β‚Š_ : Cxt β†’ Ty β†’ Cxt

length : Cxt β†’ β„•
length Ξ΅ = zero
length (Ξ“ β‚Š _) = succ (length Ξ“)

data Fin : β„• β†’ 𝓀₀ Μ‡  where
 zero : {n : β„•} β†’ Fin (succ n)
 succ : {n : β„•} β†’ Fin n β†’ Fin (succ n)

is-nonzero : β„• β†’ 𝓀₀ Μ‡
is-nonzero 0        = 𝟘
is-nonzero (succ n) = πŸ™

Fin-gives-is-nonzero : {n : β„•} β†’ Fin n β†’ is-nonzero n
Fin-gives-is-nonzero zero     = ⋆
Fin-gives-is-nonzero (succ i) = ⋆

_[_] : (Ξ“ : Cxt) β†’ Fin (length Ξ“) β†’ Ty
Ρ        [ i ] = 𝟘-elim (Fin-gives-is-nonzero i)
(xs β‚Š x) [ zero ]   = x
(xs β‚Š x) [ succ i ] = xs [ i ]

\end{code}

Terms

The term formers are the standard constants and constructors of System T:
boolean constants and conditionals, natural numbers with primitive recursion,
binary products, lambda abstraction, and application.

\begin{code}

infixl 10 _Β·_

data Tm : Cxt β†’ Ty β†’ 𝓀₀ Μ‡  where
 VAR  :  {Ξ“ : Cxt}           β†’ (i : Fin (length Ξ“)) β†’ Tm Ξ“ (Ξ“ [ i ])
 βŠ₯    :  {Ξ“ : Cxt}           β†’ Tm Ξ“ β‘‘
 ⊀    :  {Ξ“ : Cxt}           β†’ Tm Ξ“ β‘‘
 IF   :  {Ξ“ : Cxt}{Οƒ : Ty}   β†’ Tm Ξ“ (β‘‘ ⇨ Οƒ ⇨ Οƒ ⇨ Οƒ)
 ZERO :  {Ξ“ : Cxt}           β†’ Tm Ξ“ Ⓝ
 SUCC :  {Ξ“ : Cxt}           β†’ Tm Ξ“ (Ⓝ ⇨ Ⓝ)
 REC  :  {Ξ“ : Cxt}{Οƒ : Ty}   β†’ Tm Ξ“ (Οƒ ⇨ (Ⓝ ⇨ Οƒ ⇨ Οƒ) ⇨ Ⓝ ⇨ Οƒ)
 PAIR :  {Ξ“ : Cxt}{Οƒ Ο„ : Ty} β†’ Tm Ξ“ Οƒ β†’ Tm Ξ“ Ο„ β†’ Tm Ξ“ (Οƒ ⊠ Ο„)
 PRJ₁ :  {Ξ“ : Cxt}{Οƒ Ο„ : Ty} β†’ Tm Ξ“ (Οƒ ⊠ Ο„) β†’ Tm Ξ“ Οƒ
 PRJβ‚‚ :  {Ξ“ : Cxt}{Οƒ Ο„ : Ty} β†’ Tm Ξ“ (Οƒ ⊠ Ο„) β†’ Tm Ξ“ Ο„
 LAM  :  {Ξ“ : Cxt}{Οƒ Ο„ : Ty} β†’ Tm (Ξ“ β‚Š Οƒ) Ο„ β†’ Tm Ξ“ (Οƒ ⇨ Ο„)
 _Β·_  :  {Ξ“ : Cxt}{Οƒ Ο„ : Ty} β†’ Tm Ξ“ (Οƒ ⇨ Ο„) β†’ Tm Ξ“ Οƒ β†’ Tm Ξ“ Ο„

\end{code}