Fun with λ calculus

Constructors

Description Constructor
Variable Var
Application App
Abstraction / Lambda Abs

Boolean

Takes two values. The one to be given for true and false respectively.

First value is for true, second is for false.

tru λt. λf. t
fls λt. λf. f

I suppose we could also have written it like:

tru λf. λt. t
fls λf. λt. f

but then the order of arguments should be reversed as well.

—

{- Represents the boolean true value -}
-- Basically like the fst function of tuple.
-- Accepts two values and returns the first value in the pair
tru = λt. λf. t

{- Represents the boolean false value -}
-- Like snd function of tuple.
-- Accepts two values and returns the second value in the pair
fls = λt. λf. f

Constants

Representable as identity functions..

λx. c

ie, the value of the 'argument' x is simply ignored.

Natural numbers

There are many ways. Like Church encoding and Scott encoding.

Church encoding:

0 λs. λz. z
1 λs. λz. s (s z)
2 λs. λz. s (s (s z))
3 λs. λz. s (s (s (s z)))

Addition:

add =
λm n s z.
  m s (n s z)

Example:

  add (λs z. s s z) (λs z. s s s z)
= λs z. (λs z. s s z) s [(λs z. s s s z) s z]
= λs z. (λs z. s s z) s [s s s z]
= λs z. s s s s s z

Increment:

incr = λn s z. n s (s z)

—

C₀ = λs. λz. z         -- 0
C₁ = λs. λz. s z       -- S 0 = 1
C₂ = λs. λz. s (s z)   -- S (S 0) = 2

-- System F type for C could be:
-- ∀X. (X -> X) -> X -> X
--     |      |    |    |
--     ----↓---    ↓    ↓
--         s       z    result

ie, the encoding for each natural number takes two values as arguments:

which obviously can be thought of as constructors of ℕ.

I suppose we could say that their types are sort of like:

The outermost lambda gets applied first.

if statement

Could be made like

λc. λt. λe. c t e

 - c: condition
 - t: true case
 - e: else case

Here, the c is like a boolean.

As an aside, the λc. λt. λe. c t e here is constructed like

Lambda

—

{- Represents something like a condition check?? -}
if cond then else
 = test λc. λt. λe. c t e

-- An example
test λl. λm. λn. l m n

test tru v w
 ↓
(λm. λn. (tru m n)) v w
 ↓
(λn. (tru v n)) w
 ↓
(tru v w)
 ↓↓
(λt. λf. t) v w
 ↓
(λf. v) w
 ↓
v
--

Logical operations

{- logical or -}
or = λa. λb. a tru b

{-
| a   | b   | or a b            |
|-----+-----+-------------------|
| tru | tru | tru tru tru = tru |
| tru | fls | tru tru fls = tru |
| fls | tru | fls tru tru = tru |
| fls | fls | fls tru fls = fls |
-}

{- logical and -}
and = λa. λb. a b fls

{-
| a   | b   | and a b           |
|-----+-----+-------------------|
| tru | tru | tru tru fls = tru |
| tru | fls | tru fls fls = fls |
| fls | tru | fls tru fls = fls |
| fls | fls | fls fls fls = fls |
-}

{- logical not -}
and = λa. a fls tru

{-
| a   | not a             |
|-----+-------------------|
| tru | tru fls tru = fls |
| fls | fls fls tru = tru |
-}

Pairs (2-tuple)

pair = λf. λs. λb. b f s
fst = λp. p tru
snd = λp. p fls

ie, for example,

pair 1 2
= λb. b 1 2

fst (pair 1 2)
= (pair 1 2) tru
= (λb. b 1 2) tru
= tru 1 2
= (λt. λf. t) 1 2
= 1

Semantics

Syntax says how the terms can be made. Se qualifiedmantics specifies how the terms are evaluated.

Conventions

As used in TAPL.