SKI-computable functions

This file defines the notion of SKI-computability for partial functions on natural numbers, via Church numerals: a term computes f : ℕ →. ℕ if it maps Church numeral inputs to Church numeral outputs wherever f is defined.

Main definitions

• SKI.Computes: an SKI term computes a given partial function.
• SKI.Computable: a partial function is SKI-computable if some SKI term computes it.

Implementation notes

Unlike Cslib.URM.Computes, which is a two-sided equality of Part values, this predicate is one-sided: it constrains the term's behavior only where the function is defined, and says nothing about inputs outside the domain.

def Cslib.SKI.Computes (t : SKI) (f : ℕ →. ℕ) : Prop

An SKI term t computes a partial function f : ℕ →. ℕ if, for every Church numeral input, t applied to the input is a Church numeral for the output whenever f is defined.

Equations

• t.Computes f = ∀ (n : ℕ) (cn : Cslib.SKI), Cslib.SKI.IsChurch n cn → ∀ m ∈ f n, Cslib.SKI.IsChurch m (t.app cn)

def Cslib.SKI.Computable (f : ℕ →. ℕ) : Prop

A partial function f : ℕ →. ℕ is SKI-computable if there exists an SKI term that computes it.

Equations

• Cslib.SKI.Computable f = ∃ (t : Cslib.SKI), t.Computes f

theorem Cslib.SKI.computes_of_total {t : SKI} {f : ℕ →. ℕ} (g : ℕ → ℕ) (heval : ∀ (n : ℕ), f n = Part.some (g n)) (hcorrect : ∀ (n : ℕ) (cn : SKI), IsChurch n cn → IsChurch (g n) (t.app cn)) : t.Computes f

To show that a term computes a total function, it suffices to produce a Church numeral for the output on every input.

theorem Cslib.SKI.comp_computes {f g : ℕ →. ℕ} {tf tg : SKI} (hf : tf.Computes f) (hg : tg.Computes g) : ((B.app tf).app tg).Computes (f.comp g)

Composition of computable functions is computable.

theorem Cslib.SKI.pair_computes {f g : ℕ →. ℕ} {tf tg : SKI} (hf : tf.Computes f) (hg : tg.Computes g) : ((S.app ((B.app NatPair).app tf)).app tg).Computes fun (n : ℕ) => Nat.pair <$> f n <*> g n

Pairing of computable functions is computable.