2 setecho. DEFINE C0 == pop; Csucc == [dup [i] dip] dip i. DEFINE Peano == 0 [succ]. Peano C0. Peano [C0] Csucc. Peano [[C0] Csucc] Csucc. Peano [[[C0] Csucc] Csucc] Csucc. DEFINE C1 == [C0] Csucc; C2 == [C1] Csucc; C3 == [C2] Csucc. Peano C0. Peano C1. Peano C2. Peano C3. DEFINE Doublings == 1 [2 *]; Lists == [] [[i] swoncat]. Doublings C0. Doublings C1. Doublings C2. Doublings C3. Lists C0. Lists C1. Lists C2. Lists C3. DEFINE Cadd == [ [[Csucc] cons] ] dip i i; Cmul == [ [[C0]] dip [Cadd] cons [cons] cons ] dip i i; Cpow == [ [[C1 ]] dip [Cmul] cons [cons] cons ] dip i i. Peano [C2] [C3] Cadd. Peano [C2] [C3] Cmul. Peano [C2] [C3] Cpow. Doublings [C2] [C3] Cadd. Doublings [C2] [C3] Cmul. Doublings [C2] [C3] Cpow. Peano [[[[[C3] Csucc] [C2] Cadd] [C3] Cmul] Csucc] [C2] Cadd . Peano [[[[[C3] Csucc] [C2] Cadd] [C3] Cmul] Csucc] [C2] Cadd 3 succ 2 + 3 * succ 2 + = . Peano [[[[C2] [C3] Cmul] [C2] Cpow] [[C2] [[C1] Csucc] Cmul] Cadd] [C2] Cadd. DEFINE Q0 == [pop]; Qsucc == [ [dup [i] dip] dip i ] cons. Peano Q0 i. Peano Q0 Qsucc i. Peano Q0 Qsucc Qsucc i. DEFINE Q1 == Q0 Qsucc; Q2 == Q1 Qsucc; Q3 == Q2 Qsucc. Peano Q0 i. Peano Q1 i. Peano Q2 i. Peano Q3 i. Q0. Q1. Q2. Q3. DEFINE Qadd == [ [[Qsucc i] cons] swap i i ] cons cons; Qmul == [ [[[Q0 i]] dip [Qadd i] cons [cons] cons] dip i i ] cons cons; Qpow == [ [[[Q1 i]] dip [Qmul i] cons [cons] cons] dip i i ] cons cons. Peano Q2 Q3 Qadd i . Peano Q2 Q3 Qmul i . Peano Q2 Q3 Qpow i . Q2 Q3 Qadd . Q2 Q3 Qmul . Q2 Q3 Qpow . Peano Q3 Qsucc Q2 Qadd Q3 Qmul Qsucc Q2 Qadd i. Peano Q3 Qsucc Q2 Qadd Q3 Qmul Qsucc Q2 Qadd i 3 succ 2 + 3 * succ 2 + = . DEFINE Ctrue == pop i; Cfalse == popd i. DEFINE Boole == ["Yes, yes"] ["No, no"]; Comparison == 2 3 [<] [>]. Boole Ctrue. Boole Cfalse. Comparison Ctrue. Comparison Cfalse. DEFINE (* Cnot == [ [Cfalse] [Ctrue] ] dip i. *) Cnot == swapd i. Boole [Ctrue] Cnot. Boole [Cfalse] Cnot. Comparison [[Ctrue] Cnot] Cnot. Comparison [[Cfalse] Cnot] Cnot. DEFINE Cor == [[Ctrue]] dipd i; Cand == [[Cfalse]] dip i. Boole [Ctrue ] [Ctrue ] Cor. Boole [Ctrue ] [Cfalse] Cor. Boole [Cfalse] [Ctrue ] Cor. Boole [Cfalse] [Cfalse] Cor. Boole [Ctrue ] [Ctrue ] Cand. Boole [Ctrue ] [Cfalse] Cand. Boole [Cfalse] [Ctrue ] Cand. Boole [Cfalse] [Cfalse] Cand. DEFINE Ceq0 == [ [Ctrue] [pop [Cfalse]] ] dip i i. Boole [C0] Ceq0 . Boole [C1] Ceq0 . Boole [C2] Ceq0 . Boole [[C0] Ceq0] [[[C2] Csucc] Ceq0] Cor. Boole [[C0] Ceq0] [[[C2] Csucc] Ceq0] Cand. DEFINE Cifte == rolldown i. Peano [[C0] Ceq0] [C2] [C3] Cifte. Peano [[C1] Ceq0] [C2] [C3] Cifte. Peano [[[C0] Ceq0] Cnot] [C2] [C3] Cifte. Peano [[[C1] Ceq0] Cnot] [C2] [C3] Cifte. Peano [Ctrue ] [[Ctrue ] [C0] [C1] Cifte] [[Ctrue ] [C2] [C3] Cifte] Cifte. Peano [Ctrue ] [[Cfalse] [C0] [C1] Cifte] [[Cfalse] [C2] [C3] Cifte] Cifte. Peano [Cfalse] [[Ctrue ] [C0] [C1] Cifte] [[Ctrue ] [C2] [C3] Cifte] Cifte. Peano [Cfalse] [[Cfalse] [C0] [C1] Cifte] [[Cfalse] [C2] [C3] Cifte] Cifte. DEFINE Ccons == [i]; Ccar == [Ctrue] swap i; Ccdr == [Cfalse] swap i. Peano [C0] [C1] Ccons Ccar. Peano [C0] [C1] Ccons Ccdr. Peano [[C0] [C1] Ccons Ccar] [[C2] [C3] Ccons Ccar] Ccons Ccar. Peano [[C0] [C1] Ccons Ccdr] [[C2] [C3] Ccons Ccdr] Ccons Ccar. Peano [[C0] [C1] Ccons Ccar] [[C2] [C3] Ccons Ccar] Ccons Ccdr. Peano [[C0] [C1] Ccons Ccdr] [[C2] [C3] Ccons Ccdr] Ccons Ccdr. # The definition of Brent Kerby's more elegant Church numerals # The original definitions, commented away, are given for comparison. # The new definitions over-ride the old ones. DEFINE # Csucc == [dup [i] dip] dip i; Csucc == [dup dip] dip i; # Cadd == [ [[Csucc] cons] ] dip i i; Cadd == [sip] dip i; # but sip needs to be defined: sip == dupd dip; # Cmul == [ [[C0]] dip [Cadd] cons [cons] cons ] dip i i; Cmul == [cons] dip i; # Cpow == [ [[C1]] dip [Cmul] cons [cons] cons ] dip i i; Cpow == [[cons] cons] dip i i. # Now the old tests using the new definitions: Peano [C2] [C3] Cadd. Peano [C2] [C3] Cmul. Peano [C2] [C3] Cpow. Doublings [C2] [C3] Cadd. Doublings [C2] [C3] Cmul. Doublings [C2] [C3] Cpow. Peano [[[[[C3] Csucc] [C2] Cadd] [C3] Cmul] Csucc] [C2] Cadd . Peano [[[[[C3] Csucc] [C2] Cadd] [C3] Cmul] Csucc] [C2] Cadd 3 succ 2 + 3 * succ 2 + = .