ΥɥȤ򼨤Ƥޤ. lambda> ϥץץȵǤ.
ʤ׻ؽݤλͤˤƤ.
    ---------------------------------------------------------
    ϥХåå(\)ɽƤޤ.
    ޥȤ <true> Τ褦ʵɽƤޤ.
       (ޥȤñʤʸִǤ.)
    ܺ٤ :? ɽإץå򻲾ȤƤ.
    ---------------------------------------------------------

Ƥΰ
----------
  ˤߤʤ
  ߤʤ Σ
  ߤʤ Σ
  Church-Rosserǧ
  ǺΥƥå׼¹
   -- M[x:=N] ޤ [N/x]M
  μͳѿ
  黻
  βû
  Ƶ
  pair -- car, cdr, cons
  ʬŬ
  ؿ
  ޥ
  ׻̤ɽѹ
  ȥ졼


ˤߤʤ
lambda> (\x.y)((\x.xx)(\x.xx)) ->
    [1] y
    [2] (\x.y)((\x.xx)\x.xx)
    number or quit? 1                        [1] ϤǤ
lambda> (\x.y)((\x.xx)(\x.xx)) ->
    [1] y
    [2] (\x.y)((\x.xx)\x.xx)
    number or quit? 2                        [2] ֤ߤʤ
    [1] y
    [2] (\x.y)((\x.xx)\x.xx)
    number or quit? 2
    [1] y
    [2] (\x.y)((\x.xx)\x.xx)
    number or quit? 2
    [1] y
    [2] (\x.y)((\x.xx)\x.xx)
    number or quit? 1

ߤʤ Σ
lambda> (\x.xx)(\x.xx) ->
    [1] (\x.xx)\x.xx                     ̤Ѳʤߤʤ
    number or quit?
    [1] (\x.xx)\x.xx
    number or quit?
    [1] (\x.xx)\x.xx
    number or quit? q

ߤʤ Σ
lambda> (\x.xxx)(\x.xxx) ->
    [1] ((\x.xxx)\x.xxx)\x.xxx           ̤ʣˤʤ
    number or quit?
    [1] (((\x.xxx)\x.xxx)\x.xxx)\x.xxx
    number or quit?
    [1] ((((\x.xxx)\x.xxx)\x.xxx)\x.xxx)\x.xxx
    number or quit?
    [1] (((((\x.xxx)\x.xxx)\x.xxx)\x.xxx)\x.xxx)\x.xxx
    number or quit? q

Church-Rosserǧ
lambda> (\y.y((\a.xa)(\a.a)))(\b.b) ->        [2],[1] ־
    [1] (\b.b)((\a.xa)\a.a)
    [2] (\y.y(x\a.a))\b.b
    number or quit? 2
    [1] (\b.b)(x\a.a)
    number or quit? 1
    [1] x\a.a
    number or quit?
lambda> (\y.y((\a.xa)(\a.a)))(\b.b) ->        [1],[2] ־
    [1] (\b.b)((\a.xa)\a.a)
    [2] (\y.y(x\a.a))\b.b
    number or quit? 1
    [1] (\a.xa)\a.a
    [2] (\b.b)(x\a.a)
    number or quit? 2
    [1] x\a.a
    number or quit?
lambda> (\y.y((\a.xa)(\a.a)))(\b.b) ->        [1],[1] ־
    [1] (\b.b)((\a.xa)\a.a)
    [2] (\y.y(x\a.a))\b.b
    number or quit? 1
    [1] (\a.xa)\a.a
    [2] (\b.b)(x\a.a)
    number or quit? 1
    [1] x\a.a
    number or quit?

ǺΥƥå׼¹
  ׻ϵ => ꤹȺǺΤߤΥƥå׼¹ԤȤʤ.
  Ʊͤε -> ϲǽʤ٤ƤΣƥå״̤Ϥ뤿ʣ
  η̤Ϥ뤳Ȥ.
  ʤǽŪ˿ʤ뤫ɤ䤤碌Τ s ޤ c Ǳ
  뤳. ԤΤߤʤ s Ȥߤʤ.

lambda> (\xsz.s(xs(s(xsz))))(\sz.s(sz)) =>
stepwise or continuously? s                s ޤ϶Ԥǥƥå׼¹ԤȤʤ
    \sz.s((\sz.s(sz))s(s((\sz.s(sz))sz)))
    ENTER or quit?
    \sz.s((\z.s(sz))(s((\sz.s(sz))sz)))
    ENTER or quit?
    \sz.s(s(s(s((\sz.s(sz))sz))))
    ENTER or quit?
    \sz.s(s(s(s((\z.s(sz))z))))
    ENTER or quit?
    \sz.s(s(s(s(s(sz)))))
    ENTER or quit?

lambda> (\xsz.s(xs(s(xsz))))(\sz.s(sz)) =>
stepwise or continuously? c                c ξä׻
-> \sz.s((\sz.s(sz))s(s((\sz.s(sz))sz)))
-> \sz.s((\z.s(sz))(s((\sz.s(sz))sz)))
-> \sz.s(s(s(s((\sz.s(sz))sz))))
-> \sz.s(s(s(s((\z.s(sz))z))))
-> \sz.s(s(s(s(s(sz)))))

 -- M[x:=N] ޤ [N/x]M
  ѴʬǽǽǤ.
  M[x:=N] ޤ [N/x]M ηǻꤹ뤳. [ ] := / ʤɤεϥ
  ǤϻȤʤ̤Ǥ.

lambda> \sz.s(nsz)[n:=\xy.x(xy)];
\sz.s((\xy.x(xy))sz)

lambda> [\xy.x(xy)/n]\sz.s(nsz);
\sz.s((\xy.x(xy))sz)

lambda> \sz.s(nsz)[n:=<2>];
\sz.s(<2>sz)

μͳѿ
  μͳѿ򸫤Ĥ뵡ǽ :print FV() Ǥ.

lambda> :p FV(\xy.mx(ny))         :p  :print ξά
{m, n}

黻
  ѤߤΥޥɽˤ :macro(ޤ:m) Ϥ뤳.

lambda> <not><false>;
<true>
3 step(s) [0.000ms]
lambda> <not><true>;
<false>
3 step(s) [0.000ms]
lambda> <and><false><false>;
<false>
4 step(s) [0.000ms]
lambda> <and><false><true>;
<false>
4 step(s) [0.018ms]
lambda> <and><true><false>;
<false>
4 step(s) [0.000ms]
lambda> <and><true><true>;
<true>
4 step(s) [0.000ms]
lambda> <or><false><false>;
<false>
4 step(s) [0.000ms]
lambda> <or><false><true>;
<true>
4 step(s) [0.000ms]
lambda> <or><true><false>;
<true>
4 step(s) [0.001ms]
lambda> <or><true><true>;
<true>
4 step(s) [0.002ms]

βû
  ѤߤΥޥɽˤ :macro(ޤ:m) Ϥ뤳.

lambda> <add><3><2> ;
<5>                          3 + 2 = 5
6 step(s) [0.000ms]
lambda> <add><3><2> ->
    [1] (\nsz.<3>s(nsz))<2>
    number or quit?
    [1] \sz.<3>s(<2>sz)
    [2] (\nsz.(\z.s(s(sz)))(nsz))<2>
    number or quit?
    [1] \sz.(\z.s(s(sz)))(<2>sz)
    [2] \sz.<3>s((\z.s(sz))z)
    number or quit?
    [1] \sz.s(s(s(<2>sz)))
    [2] \sz.(\z.s(s(sz)))((\z.s(sz))z)
    number or quit?
    [1] \sz.s(s(s((\z.s(sz))z)))
    number or quit?
    [1] <5>
    number or quit?

Ƶ
  ѤߤΥޥɽˤ :macro(ޤ:m) Ϥ뤳.

lambda> <Y><fact><3>;          Curryư黻ҤȤä
<6>
694 step(s) [0.858ms]
lambda> <Yt><fact><3>;         Turingư黻ҤȤä
<6>
709 step(s) [0.400ms]

pair -- car, cdr, cons
  ѤߤΥޥɽˤ :macro(ޤ:m) Ϥ뤳.

lambda> <car>(<cons>XY);
X
6 step(s) [0.000ms]
lambda> <cdr>(<cons>XY);
Y
6 step(s) [0.003ms]

ʬŬ
  Ȥ
      (\mn.m+n)3 -> \n.3+n
  򼨤.  +  3 ʤάˡȤäƤ뤳Ȥ.
  ̣
      ѿؿ \mn.m+n ʬŬѤȣѿؿ \n.3+n ˤʤ
  Ȥ.

lambda> (\mnsz.ms(nsz))<3>;         άˡ (\mn.m+n)3
\nsz.s(s(s(nsz)))                   άˡ \n.3+n
3 step(s) [0.002ms]

  ºݤˤ줬ˣûؿȤʤäƤ뤳Ȥǧ뤿
      (\n.3+n)2 -> 5
  Ȥʤ뤳Ȥ򼨤.

lambda> (\nsz.s(s(s(nsz))))<2>;        άˡ (\n.3+n)2
<5>                                    άˡ 5
3 step(s) [0.001ms]

ؿ
  ؿ f  g δؿ \fgx.g(fx) ɽǤ.
  ŪʣĤδؿ
      add1 = <add><1> = (\mnsz.ms(nsz))(\sz.sz)    άˡ \x.1+x
      mul2 = <mul><2> = (\mns.m(ns))(\sz.s(sz))      άˡ \x.2*x
  δؿ
      (\fgx.g(fx))<add1><mul2>                      άˡ \x.2*(1+x)
  Ȥʤ.

lambda> (\fgx.g(fx))((\mnsz.ms(nsz))<1>)((\mns.m(ns))<2>);
\xsz.s(xs(s(xsz)))
17 step(s) [0.002ms]

  ºݤˤ줬ҤιؿȤʤäƤ뤳Ȥǧ뤿
      (\x.2*(1+x))5 -> 12
  Ȥʤ뤳Ȥ򼨤.

lambda> (\xsz.s(xs(s(xsz))))<5>;    άˡ (\x.2*(1+x))5
<12>                                άˡ 12
5 step(s) [0.001ms]

ޥ
  ޥΥ󥿥
      ޥ̾ =  ;
  Ǥ.
  ե˥ޥ򵭽ҤƤϲˡǥɤǤ.
    (1) :load ޥɤǼ¹ɤ߹.
    (2) ޥɹ԰ -l ץǵưɤ߹.

lambda> add1mul = \xsz.s(xs(s(xsz)));       άˡ \x.2*(1+x)
lambda> <add1mul><3>;
<8>                                         άˡ 8
5 step(s) [0.000ms]

lambda> :load macrofile     ե뤫ޥɤ߹.

׻̤ɽѹ
  ̤Ϥݤ :format ޥɤɽѹǤ.
  :format ޥɤΰȤƲǽͤϼΤȤ.
         abbrev ǤʷʿŪɽ   [] xy.xyz
         math   ʷ̾οŪɽ [] x.y.xyz
         proper ̤¿Ūɽ   [] x.(y.((xy)z))
   :reshape ޥɤǷ̤ʸޥ֤̾뤫ɤ
  Ǥ. ǥեưϥޥ֤̾.

lambda> :format proper
lambda> \xy.xyz;
\x.(\y.((xy)z))           ̤¿ι¤Τˤʤ.
0 step(s) [0.001ms]
lambda> :f math
lambda> \xy.xyz;
\x.\y.xyz                 ݤɽ.
0 step(s) [0.000ms]
lambda> :f abbrev
lambda> \xy.xyz;
\xy.xyz                   ̾ϤηǽϤ.
0 step(s) [0.000ms]

lambda> :reshape off      ޥ֤̾ʤ
lambda> <Y><fact><3>;
\sz.s(s(s(s(s(sz)))))      <6> ̣.
694 step(s) [0.762ms]
lambda> :r                ޥ֤̾
lambda> <Y><fact><3>;
<6>                       ̤Ѥߥޥ֤Ƥ.
694 step(s) [0.761ms]

ȥ졼
  :trace ޥɤǥȥ졼ϤǤ.
  ȥ졼Ϥ
    ->ϴ̤ɽ.
    ǥȤʬη׻Ǥ뤳Ȥɽ.
    --ϳѴε§ɽ. (׻ ⶶ p.65)

lambda> :t              ȥ졼ϳ
lambda> <succ><3>;
<succ><3>
  \sz.s(nsz)[n:=<3>]  -- (x.M)NM[x:=N]
-> \sz.s(<3>sz)
\sz.s(<3>sz)
  \z.s(<3>sz)  -- x.Mx.N if MN
    s(<3>sz)  -- x.Mx.N if MN
      <3>sz  -- PMPN if MN
        <3>s  -- MPNP if MN
          \z.s(s(sz))[s:=s]  -- (x.M)NM[x:=N]
        -> \z.s(s(sz))  -- MPNP if MN
      -> (\z.s(s(sz)))z  -- PMPN if MN
    -> s((\z.s(s(sz)))z)  -- x.Mx.N if MN
  -> \z.s((\z.s(s(sz)))z)  -- x.Mx.N if MN
-> \sz.s((\z.s(s(sz)))z)
\sz.s((\z.s(s(sz)))z)
  \z.s((\z.s(s(sz)))z)  -- x.Mx.N if MN
    s((\z.s(s(sz)))z)  -- x.Mx.N if MN
      (\z.s(s(sz)))z  -- PMPN if MN
        s(s(sz))[z:=z]  -- (x.M)NM[x:=N]
      -> s(s(sz))  -- PMPN if MN
    -> s(s(s(sz)))  -- x.Mx.N if MN
  -> \z.s(s(s(sz)))  -- x.Mx.N if MN
-> <4>
<4>
3 step(s) [0.008ms]

lambda> :t off          ȥ졼
lambda> <succ><3>;
<4>
3 step(s) [0.000ms]

