-- ޥ
--  []
--   ХååϦˤ̣. פΰ̣ǤϤʤ.
--   "--"ǻϤޤԤϥȤȤʤ.
{-
     εϥץѥƥѹǤΤդ뤳.
     -----------------------------------------------
       =   ޥ̾ͤζڤ
       ;   ޥνλ
       <   ޥȤγ
       >   ޥȤνλ
-}

true   = \tf.t;
false  = \tf.f;
and    = \pq.pq<false>;
or     = \pq.p<true>q;
not    = \p.p<false><true>;
if     = \pxy.pxy;
succ   = \nsz.s(nsz);
pred   = \nsz.n(\gh.h(gs))(\u.z)(\u.u);
add    = \mnsz.ms(nsz);
plus   = <add>;
sub    = \mn.n<pred>m;
mul    = \mns.m(ns);
exp    = \mn.nm;
iszero = \n.n(\x.(\tf.f))(\tf.t);

I      = \x.x;
K      = \xy.x;
S      = \xyz.xz(yz);
-- Curryư黻
Y      = \f.(\x.f(xx))(\x.f(xx));
-- Turingư黻
Yt     = (\zx.x(zzx))(\zx.x(zzx));

car    = \p.p<true>;     -- car[(a.b)] = a
cdr    = \p.p<false>;    -- cdr[(a.b)] = b
cons   = \fsb.bfs;       -- cons[a;b] = (a.b)

{-
  ͤϥץǺФ褦˲ɤ줿ΤǥȤȤ.
	0      = \sz.z;
	1      = \sz.sz;
	2      = \sz.s(sz);
	3      = \sz.s(s(sz));
	4      = \sz.s(s(s(sz)));
	5      = \sz.s(s(s(s(sz))));
	6      = \sz.s(s(s(s(s(sz)))));
	7      = \sz.s(s(s(s(s(s(sz))))));
	8      = \sz.s(s(s(s(s(s(s(sz)))))));
	9      = \sz.s(s(s(s(s(s(s(s(sz))))))));
	10     = \sz.s(s(s(s(s(s(s(s(s(sz)))))))));
	11     = \sz.s(s(s(s(s(s(s(s(s(s(sz))))))))));
-}

{-
   
    lambda> <Y><fact><1>;
    \sz.sz
    36 step(s) [0.003ms]
    lambda> <Y><fact><2>;
    \sz.s(sz)
    142 step(s) [0.041ms]
    lambda> <Y><fact><3>;
    \sz.s(s(s(s(s(sz)))))
    694 step(s) [0.711ms]
    lambda> <Y><fact><4>;
    \sz.s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(sz)))))))))))))))))))))))
    4068 step(s) [9.889ms]
-}
fact   = \fx.<if>(<iszero>x)<1>(<mul>x(f(<pred>x)));
