;; -*-mode: Outline; -*- Basic Lambda Arithmetics ; \$Id: LC_basic.lhs,v 1.1 2002/04/28 20:41:44 oleg Exp oleg \$ * Preliminaries > module LC_basic where > > import Lambda_calc > import Prelude hiding ((^),and,or,not,succ) > * Basic combinators > combY = f ^ (x ^ f # (x # x)) # (x ^ f # (x # x)) > combI = x ^ x * Booleans > true = x ^ y ^ x > false = x ^ y ^ y > and = p ^ q ^ p # q # false > or = p ^ q ^ p # true # q > not = p ^ p # false # true > xor = p ^ q ^ p # (q # false # true) # q > equ = p ^ q ^ not # (xor # p # q) > --another derivation: equ = p ^ q ^ p # q # (q # false # true) ** Examples LC_basic> equ LC_basic> eval \$ equ # true # false LC_basic> eval \$ equ # false # false LC_basic> eval \$ and # false # q -- always false, regardless of q LC_basic> eval \$ and # true # q -- gives q, i.e., for each q! In other words, the reduction of (and # p # q) gives true if and only if both p and q are true. Otherwise the reduction ends up with false, just as it is supposed to. It is easy to verify that definitions for the other boolean functions are consistent with their usual meaning. ; By the way, it should be noted that LC_basic> eval \$ true # a # b --==> a LC_basic> eval \$ false # a # b --==> b i.e. our functions true and false act like the if-selector. The following is a genuine if selector, which takes a predicate and branches accordingly. * Genuine if selector > lif = p ^ x ^ y ^ p # x # y LC_basic> eval \$ lif # true # a # b -- ==> a LC_basic> eval \$ lif # false # a # b -- ==> b : for all b! * Ordered Pairs > cons = x ^ y ^ p ^ p # x # y > car = p ^ p # true > cdr = p ^ p # false The definitions above satisfy the axioms for pairs: LC_basic> eval \$ car # (cons # a # b) -- ==> a LC_basic> eval \$ cdr # (cons # a # b) -- ==> b * Basic arithmetics ** zero and its successors > c0 = f ^ x ^ x -- Church numeral 0 > succ = c ^ f ^ x ^ f # (c # f # x) -- Successor note c0 is false -- just like in C -- equal? c0 false ==> #t > c1 = eval \$ succ # c0 -- pre-evaluate other numerals > c2 = eval \$ succ # c1 > c3 = eval \$ succ # c2 > c4 = eval \$ succ # c3 LC_basic> c4 (X equal? (%succ %c0) %c1) ; ==> #f (X equal?* (%succ %c0) %c1) ; ==> #t ** addition and multiplication > add = a ^ b ^ f ^ x ^ a # f # (b # f # x) -- Add two numerals > mul = a ^ b ^ f ^ a # (b # f) -- multiplication LC_basic> eval \$ add # c1 # c2 LC_basic> eval \$ mul # c1 # a LC_basic> eval \$ mul # c1 -- an identity function LC_basic> eval \$ mul # c0 -- const 0: an Algebraic result! LC_basic> eval \$ mul # c3 # c4 ** zero checking A numeral 'cn' is represented by a function (operator) that applies any function to its argument exactly n times. Given a function "(and false)", zero applications of it to an argument true returns true, whereas applying the function one or several times to the true argument will give false. The idea does work: > zerop = c ^ c # (and # false) # true LC_basic> eval \$ zerop # c0 -- (\x. (\y. x)) LC_basic> eval \$ zerop # c1 -- (\x. (\y. y)) LC_basic> eval \$ zerop # (mul # c0 # a) -- ==> true regardless of a -- an algebraic result LC_basic> eval \$ zerop # (succ # a) -- ==> false ** exponentiation raising a to the power of b means multiplying 1 by a exactly b times. In other words, it means applying mult a operator to c1 b times. > expt = a ^ b ^ b # (mul # a) # c1 LC_basic> eval \$ expt # a # c0 --> (\f. (\x. f x)) always 1 LC_basic> eval \$ expt # a # c1 --> always a, for any a * Notes ;; Random notes ;; c1 true x -> true x ;; (X equal?* (c1 true x) (true x)) ;; true \y.x -> \v\y.x ;; (true (y ^ x)) ;; cn (\y.x) u -> x whereas c0 (\y.x) u -> u ;; (c3 (y ^ x) u) ==> x (c0 (y ^ x) u) ==> u ;; In particular, ;; cn (\y.succ) u -> succ ;; (c3 (y ^ succ) u) ==> succ