# This is a sample macro definition file of LambdaFriends.
# These macros are designed for untyped lambda-calculus.

# '#' and following characters are regarded as comments.

# Note: Following Combinators are supported as built-in macros.
# * Church Numerals : <0>, <1>, <2>, ...
# * Church Booleans : <true>, <false>
# * SKI Combinators : <S>, <K>, <I>

# Note 2: In the current version of LambdaFriends,
# once you redefine a macro,
# the previous version of the macro will be "shadowed".
# For example, if you input the following two lines:
#   M = \x.x
#   M = <M><M>
# then <M> is syntactically equivalent to (\x.x)(\x.x).

# Logical operators on Church booleans
not    = \p.p<false><true>
and    = \xy.xy<false>
or     = \xy.x<true>y
if     = \ctf.ctf

# Pairs
pair   = \xy.\p.pxy
head   = <true>
tail   = <false>
fst    = \p.p<true>
snd    = \p.p<false>

# Predecessor
prefn  = \f.\p.<pair>(f(<fst>p))(<fst>p)
pre    = \nfx.<snd>(n(<prefn>f)(<pair>xx))
pre2   = \nfx.n(\p.\y.y(f(p(\tf.t)))(p(\tf.t)))(\p.pxx)(\tf.f)
pre3   = \nfx.n(\g.\h.h(gf))(\u.x)(\u.u)

# Arithmetic operators on Church numerals
succ   = \n.\sz.s(nsz)
add    = \mn.\sz.ms(nsz)
sub    = \mn.n<pre>m
mul    = \mn.\sz.m(ns)z
exp    = \mn.nm
is0    = \n.n(\x.<false>)<true>
eq     = <Y>(\f.\nm.(<or>(<is0>n)(<is0>m))(<and>(<is0>n)(<is0>m))(f(<pre>n)(<pre>m)))
one?   = \n.n(\x.\p.p(\tf.f)(x(\tf.t)))(\p.p(\tf.t)(\tf.t))(\tf.f)

# Fixpoint Combinator
Y      = \f.(\x.f(xx))(\x.f(xx)) # this is a kind of fixed-point combinator

# Sample of recursion using Y combinator
fact   = <Y>(\g.\n.<if>(<is0> n) <1> (<mul>n(g(<pre>n))))
lt2 = \n.<or> (<is0> n) (<is0> (<pre> n))
fib = <Y>(\g.\n.<if>(<lt2> n)n(<add>(g(<sub>n<1>))(g(<sub>n<2>))))