;; -*-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