stdlib.gdl

#######################################
#                                     #
#    GödelT "Standard Library"        #
#                                     #
#  By Jonas Betzendahl, 2016          #
#     @jbetzend                       #
#  jbetzend@techfak.uni-bielefeld.de  #
#                                     #
#######################################

# Identity on natural numbers
id-Nat : (ℕ → ℕ)
id-Nat = λ(a : ℕ).a

# Addition on natural numbers
add : (ℕ → (ℕ → ℕ))
add = λ(a : ℕ).λ(b : ℕ).rec b { Z ~> a | S(c) with d ~> S(d) }

# Multiplication in natural numbers
mult : (ℕ → (ℕ → ℕ))
mult = λ(a : ℕ).λ(b : ℕ).rec a { Z ~> 0 | S(c) with d ~> ((_add_[b])[d]) }

# Factorial on natural numbers
factorial : (ℕ → ℕ)
factorial = λ(a : ℕ).rec a { Z ~> S(0) | S(b) with c ~> ((_mult_[S(b)])[c]) }

# Doubling of natural numbers
double : (ℕ → ℕ)
double = λ(a : ℕ).rec a { Z ~> Z | S(b) with c ~> S(S(c)) }

# Function composition for nat -> nat
circ : ((ℕ → ℕ) → ((ℕ → ℕ) → (ℕ → ℕ)))
circ = λ(f : (ℕ → ℕ)).λ(g : (ℕ → ℕ)).λ(x : ℕ).(f[(g[x])])

# Repeated function application
it : ((ℕ → ℕ) → (ℕ → (ℕ → ℕ)))
it = λ(f : (ℕ → ℕ)).λ(n : ℕ).rec n { Z ~> _id-Nat_ | S(x) with g ~> ((_circ_[f])[g]) }

# BOOLEANS

# Identity on natural numbers
id-Bool : (𝟚 → 𝟚)
id-Bool = λ(a : 𝟚).a

# Negation
not : (𝟚 → 𝟚)
not = λ(a : 𝟚).if a then ff else tt

# Conjunction
and : (𝟚 → (𝟚 → 𝟚))
and = λ(a : 𝟚).λ(b : 𝟚).if a then if b then tt else ff else ff

# Disjunction
or : (𝟚 → (𝟚 → 𝟚))
or = λ(a : 𝟚).λ(b : 𝟚).if a then tt else if b then tt else ff

# NOR
nor : (𝟚 → (𝟚 → 𝟚))
nor = λ(a : 𝟚).λ(b : 𝟚).(_not_[((_or_[a])[b])])

# NAND
nand : (𝟚 → (𝟚 → 𝟚))
nand = λ(a : 𝟚).λ(b : 𝟚).(_not_[((_and_[a])[b])])