# adapted from my pong_lambda project: <https://gitlab.com/mcmfb/pong_lambda>
# booleans
true = \x y -> x
false = \x y -> y
not = \b -> b false true
and = \p q -> p q false
or = \p q -> p true q
# pairs
pair = \x y z -> z x y
first = \p -> p (\x y -> x)
second = \p -> p (\x y -> y)
# combinators
id = \u -> u
const = \u v -> u
I = id
K = const
Y = \f -> (\x -> f (x x)) (\x -> f (x x))
# lists
#hd = first
#tl = second
nil = false
isEmpty = \list -> list (\head tail nilClause -> false) true
# unfortunately takes O(length of listOne) steps
append = \listOne listTwo -> Y &
(\recur l -> l &
(\head tail nilClause -> &
pair head (recur tail)) &
listTwo) &
listOne
# Evaluates the nth element of a list, starting from 0.
# If the index is < 0 or greater than the list size, evaluates to nil.
#
nth = \list num -> Y &
(\recur l !n -> l &
(\head tail nilClause -> (sign n) &
(recur tail (pred n)) &
nil &
head) &
nil) &
list num
mapList = \f list -> Y &
(\recur l -> l &
(\head tail nilClause -> &
pair (f head) (recur tail)) &
nil) &
list
# Integers.
# The encoding we use for positive numbers is somewhere between a list
# (chained church pairs) and
# the traditional church encoding for numbers.
# This allows a simple implementation for the predecessor, which takes
# O(1) reduction steps, while keeping a simple implementation for the successor
# function.
# Further, the way the predecessor function works also allows us to deal with
# negative numbers, though with some caveats; see below.
#
# To the best of my knowledge, I'm the first one to derive this encoding, and
# therefore I get to name it too. Since the positive numbers are made of Chained
# Lambdas and the negative ones, of Nested redexes with the Identity function,
# it makes sense to call it CLNI (or Chalaneid, if you want a more exotic name).
#
zero = \x -> x
succ = \n x -> n (\u -> u x)
pred = \n x -> (n x (\u -> u))
one = succ zero
two = succ one
three = succ two
four = succ three
five = succ four
six = succ five
seven = succ six
eight = succ seven
nine = succ eight
ten = succ nine
minusOne = pred zero
minusTwo = pred minusOne
minusThree = pred minusTwo
minusFour = pred minusThree
minusFive = pred minusFour
minusSix = pred minusFive
minusSeven = pred minusSix
minusEight = pred minusSeven
minusNine = pred minusEight
minusTen = pred minusNine
# This is just a generalization of true and false with 3 branches.
posSign = \x y z -> x
negSign = \x y z -> y
zeroSign = \x y z -> z
# Extract the sign of a number.
# This unfortunately takes O(n) steps on negative numbers, but, due to their
# nature, I don't think anything can be done about it.
#
sign = \n -> n (\x y -> y) (\u v w -> w) (\a b -> zeroSign) (\a -> posSign) negSign
#isPositive = \n -> (sign n) true false false
#isNegative = \n -> (sign n) false true false
# Rather than using sign directly, I've made these based off of sign.
# This also means less reduction steps.
isPositive = \n -> n (\x -> x) (\a b -> b) (\z x y -> x) (\x y -> y)
isNegative = \n -> n (\x y -> y) (\a b -> b) (\z x y -> y) (\x y -> x)
# I can't make this one any better.
isZero = \n -> (sign n) false false true
# Note: just using "\m n x -> m (n x)" wouldn't be commutative:
#
# > (\m n x -> m (n x)) minusTwo two
# = (λx. x)
# > (\m n x -> m (n x)) two minusTwo
# = (λx u. u (λu1. u1 (x (λu2. u2) (λu3. u3))))
#
# So when there first argument is positive and the second is negative we must
# swap them.
#
#add = \m n x -> (and (isPositive m) (isNegative n)) (n (m x)) (m (n x))
#
# ... but it's not wrong to swap the arguments every time the second one is
# negative. This means less reductions.
#
add = \m n x -> (isNegative n) (n (m x)) (m (n x))
# invert the signal of a number.
minus = \n -> applyNTimes n zero pred succ
# if m > 0, compute f (f ... (f n) ...) with m f's.
# if m < 0, compute g (g ... (g n) ...) with abs(m) g's.
#
# In other words, this converts a number in our encoding to Church encoding,
# using the sign to choose between two functions that may be applied.
#
applyNTimes = \m n f g -> &
Y (\r !a b -> (sign a) &
(r (pred a) (f b)) &
(r (succ a) (g b)) &
b &
) m n
sub = \m n -> add m (minus n)
# Three-way comparison.
#
#cmp = \m n -> sign (sub m n)
#
greaterThan = posSign
lesserThan = negSign
equalTo = zeroSign
cmp = \m n -> &
(Y (\recur !a !b -> (sign a) &
((isPositive b) &
(recur (pred a) (pred b)) &
greaterThan) &
((isNegative b) &
(recur (succ a) (succ b)) &
lesserThan) &
((sign b) &
lesserThan &
greaterThan &
equalTo)) &
m n)
# Two-way comparisons, implemented in terms of the three-way one.
#
lt = \m n -> (cmp m n) false true false
gt = \m n -> (cmp m n) true false false
eq = \m n -> (cmp m n) false false true
leq = \m n -> (cmp m n) false true true
geq = \m n -> (cmp m n) true false true
mul = \m n -> applyNTimes m zero (add n) (add (minus n))
square = \x -> mul x x
# Integer division.
# divPos is a function and divide two strictly positive numbers.
# This function gives one when dividing by zero, arbitrarily.
#
div = \m n -> (sign m) &
((sign n) &
(divPos m n) &
(minus (divPos m (minus n))) &
one) &
((sign n) &
(minus (divPos (minus m) n)) &
(divPos (minus m) (minus n)) &
one) &
zero
# This function may loop indefinitely if given any non-positive arguments.
#
divPos = \!m !n -> actualDivPos m n zero
actualDivPos = \a b quot -> &
Y (\recur !m !n !q -> &
(\!diff -> (isNegative diff) &
q &
(recur diff n (succ q))) &
((\!minusN -> add m minusN) (minus n)) &
) a b quot
# Another implementation of division; takes way too many reductions.
# compute the list of all powers of ten smaller than x.
#powersOfTenNotGreater = \num -> &
# Y (\recur !x !pow !list -> &
# (gt pow x) &
# list &
# (recur x (mul pow ten) (pair pow list)) &
# ) num one nil
# subtract subFrom from num as many times as possible while keeping the result
# positive, incrementing acc by addBy each time, returning the pair (num, acc)
# after this.
# This function assumes num > 0 on the first call.
#
#subAcc = \num acc addBy subFrom -> &
# Y (\recur !x !a -> &
# (lt x subFrom) &
# (pair a x) &
# (recur (sub x subFrom) (add a addBy)) &
# ) num acc
#divPos = \a b -> &
# Y (\recur !l !p -> &
# l (\h t d -> recur t (subAcc (second p) (first p) h (mul b h))) &
# (first p) &
# ) (powersOfTenNotGreater a) (pair zero a)