-
-
Save zelinskiy/519741c3a66efd6d4015f01be49d2768 to your computer and use it in GitHub Desktop.
System T, a formulation of Church's Simple Theory of Types in Agda. From ~( http://publish.uwo.ca/~jbell/types.pdf ); Church's paper at ~( https://www.classes.cs.uchicago.edu/archive/2007/spring/32001-1/papers/church-1940.pdf )
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {- A straightforward version of Church’s simple type theory is the following system T -} | |
| module T where | |
| open import Data.Nat | |
| -- The type of contexts. | |
| data Γ (X : Set) : Set where | |
| ε : Γ X | |
| _::_ : (γ : Γ X) → X → Γ X | |
| infixl 4 _::_ | |
| -- Types: | |
| data Type : Set where | |
| Ι : Type -- The type of individuals | |
| Ω : Type -- The type of propositions | |
| _==>_ : Type → Type → Type -- Function types | |
| infixr 4 _==>_ | |
| -- Variables (using de Bruijn Indexes). | |
| data Var : Set where | |
| mkVar : ℕ → Var | |
| -- Terms: | |
| data Term : Set where | |
| var : Var → Term -- Variables | |
| _[_] : Term → Term → Term -- Function Application | |
| Λ_∙_ : Var → Term → Term -- λ Abstraction | |
| _==_ : Term → Term → Term -- Equality | |
| -- Extension of T by Henkin [1963] | |
| ⊤ : Term | |
| ⊥ : Term | |
| _⇒_ : Term → Term → Term | |
| _∧_ : Term → Term → Term | |
| _∨_ : Term → Term → Term | |
| for_all : Var → Type → Term → Term | |
| exist : Var → Type → Term → Term | |
| open import Data.Product | |
| data _∈_ (t : (Var × Type)) : Γ (Var × Type) → Set where | |
| here : ∀ {Γ} → t ∈ (Γ :: t) | |
| there : ∀ {Γ σ} → t ∈ Γ → t ∈ (Γ :: σ) | |
| infix 3 _∈_ | |
| data _⊢_∶_ : Γ (Var × Type) → Term → Type → Set where | |
| var : {γ : Γ (Var × Type)}{x : Var}{τ : Type} → | |
| (x , τ) ∈ γ → | |
| ----------------- | |
| γ ⊢ var x ∶ τ | |
| lam : {γ : Γ (Var × Type)}{x : Var}{M : Term}{σ τ : Type} → | |
| (γ :: (x , τ)) ⊢ M ∶ σ → | |
| --------------- | |
| γ ⊢ Λ x ∙ M ∶ (σ ==> τ) | |
| app : {γ : Γ (Var × Type)}{M N : Term}{σ τ : Type} → | |
| (γ ⊢ M ∶ (σ ==> τ)) → | |
| γ ⊢ N ∶ σ → | |
| --------------------- | |
| γ ⊢ M [ N ] ∶ τ | |
| eq : {γ : Γ (Var × Type)}{t u : Term}{α : Type} → | |
| (γ ⊢ t ∶ α) → | |
| (γ ⊢ u ∶ α) → | |
| -------------- | |
| (γ ⊢ t == u ∶ Ω) | |
| true : {γ : Γ (Var × Type)} → | |
| ---------------------- | |
| (γ ⊢ ⊤ ∶ Ω) | |
| falsum : {γ : Γ (Var × Type)} → | |
| ---------------------- | |
| (γ ⊢ ⊥ ∶ Ω) | |
| impl : {γ : Γ (Var × Type)}{α β : Term} → | |
| (γ ⊢ α ∶ Ω) → | |
| (γ ⊢ β ∶ Ω) → | |
| -------------- | |
| (γ ⊢ α ⇒ β ∶ Ω) | |
| conj : {γ : Γ (Var × Type)}{α β : Term} → | |
| (γ ⊢ α ∶ Ω) → | |
| (γ ⊢ β ∶ Ω) → | |
| -------------- | |
| (γ ⊢ α ∧ β ∶ Ω) | |
| disj : {γ : Γ (Var × Type)}{α β : Term} → | |
| (γ ⊢ α ∶ Ω) → | |
| (γ ⊢ β ∶ Ω) → | |
| -------------- | |
| (γ ⊢ α ∨ β ∶ Ω) | |
| for_all : {γ : Γ (Var × Type)}{x : Var}{τ : Type}{α : Term} → | |
| (γ :: (x , τ)) ⊢ α ∶ Ω → | |
| ------------------------- | |
| (γ ⊢ for_all x τ α ∶ Ω) | |
| exist : {γ : Γ (Var × Type)}{x : Var}{τ : Type}{α : Term} → | |
| (γ :: (x , τ)) ⊢ α ∶ Ω → | |
| ------------------------- | |
| (γ ⊢ exist x τ α ∶ Ω) | |
| infix 3 _⊢_∶_ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment