65 lines
2.6 KiB
Text
65 lines
2.6 KiB
Text
|
-- without recursion, computation is kind of hard
|
||
|
|
-- we can, however, define natural numbers using the Church encoding and do
|
||
|
|
-- computation with them
|
||
|
|
|
||
|
|
-- the natural number `n` is encoded as the function taking any function
|
||
|
|
-- `A -> A` and repeating it `n` times
|
||
|
|
nat : * := forall (A : *), (A -> A) -> A -> A;
|
||
|
|
|
||
|
|
-- zero is the constant function
|
||
|
|
zero : nat := fun (A : *) (f : A -> A) (x : A) => x;
|
||
|
|
|
||
|
|
-- `suc n` composes one more `f` than `n`
|
||
|
|
suc : nat -> nat := fun (n : nat) (A : *) (f : A -> A) (x : A) => f ((n A f) x);
|
||
|
|
|
||
|
|
-- addition can be encoded as usual
|
||
|
|
plus : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A f) (n A f x);
|
||
|
|
|
||
|
|
-- likewise for multiplication
|
||
|
|
times : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A (n A f)) x;
|
||
|
|
|
||
|
|
-- unforunately, it is impossible to prove induction on Church numerals,
|
||
|
|
-- which makes it really hard to prove standard theorems, or do anything really.
|
||
|
|
|
||
|
|
-- but we can still do computations with Church numerals
|
||
|
|
|
||
|
|
-- first some abbreviations for numbers will be handy
|
||
|
|
one : nat := suc zero;
|
||
|
|
two : nat := suc one;
|
||
|
|
three : nat := suc two;
|
||
|
|
four : nat := suc three;
|
||
|
|
five : nat := suc four;
|
||
|
|
six : nat := suc five;
|
||
|
|
seven : nat := suc six;
|
||
|
|
eight : nat := suc seven;
|
||
|
|
nine : nat := suc eight;
|
||
|
|
ten : nat := suc nine;
|
||
|
|
|
||
|
|
-- now we can do a bunch of computations, even at the type level
|
||
|
|
-- the way we can do this is by defining equality (see <examples/logic.pg> for
|
||
|
|
-- more details on how this works) and proving a bunch of theorems like
|
||
|
|
-- `plus one one = two` (how exciting!)
|
||
|
|
-- then perga will only accept our proof if `plus one one` and `two` are beta
|
||
|
|
-- equivalent
|
||
|
|
|
||
|
|
-- first we do need a definition of equality
|
||
|
|
eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
|
||
|
|
eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
|
||
|
|
eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) =>
|
||
|
|
Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy;
|
||
|
|
eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) =>
|
||
|
|
Hyz P (Hxy P Hx);
|
||
|
|
eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
|
||
|
|
fun (P : B -> *) (Hfx : P (f x)) =>
|
||
|
|
H (fun (a : A) => P (f a)) Hfx;
|
||
|
|
|
||
|
|
-- since `plus one one` and `two` are beta-equivalent, `eq_refl nat two` is a
|
||
|
|
-- proof that `1 + 1 = 2`
|
||
|
|
one_plus_one_is_two : eq nat (plus one one) two := eq_refl nat two;
|
||
|
|
|
||
|
|
-- we can likewise compute 2 + 2
|
||
|
|
two_plus_two_is_four : eq nat (plus two two) four := eq_refl nat four;
|
||
|
|
|
||
|
|
-- even multiplication works
|
||
|
|
two_times_five_is_ten : eq nat (times two five) ten := eq_refl nat ten;
|