̃hLg͑Ă܂. lambda> ̓vvgLł.
^Ȃ_vZwKۂ̎QlɂĂ.
    ---------------------------------------------------------
    _L̓obNXbV(\)ŕ\Ă܂.
    }NQƂ <true> ̂悤ȋLŕ\Ă܂.
       (}NƂ͒PȂ镶uł.)
    ڍׂ :? ŕ\wvbZ[WQƂĂ.
    ---------------------------------------------------------

ëꗗ
----------
  Ȗ菇ɂ~Ȃ
  ~Ȃ ̂P
  ~Ȃ ̂Q
  Church-Rosser̒藝mF
  ōȖ̃Xebvs
   -- M[x:=N] ܂ [N/x]M
  _̎Rϐo
  _Z
  ̉Z
  ċA
  pair -- car, cdr, cons
  Kp
  ֐
  }N`
  vZʂ̕\ύX
  g[X


Ȗ菇ɂ~Ȃ
lambda> (\x.y)((\x.xx)(\x.xx)) ->
    [1] y
    [2] (\x.y)((\x.xx)\x.xx)
    number or quit? 1                        [1] ͂łɐK`
lambda> (\x.y)((\x.xx)(\x.xx)) ->
    [1] y
    [2] (\x.y)((\x.xx)\x.xx)
    number or quit? 2                        [2] IԂƒ~Ȃ
    [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

~Ȃ ̂P
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

~Ȃ ̂Q
lambda> (\x.xxx)(\x.xxx) ->
    [1] ((\x.xxx)\x.xxx)\x.xxx           Ȗ񌋉ʂ蕡GɂȂ
    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̒藝mF
lambda> (\y.y((\a.xa)(\a.a)))(\b.b) ->        [2],[1] Iԏꍇ
    [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] Iԏꍇ
    [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] Iԏꍇ
    [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?

ōȖ̃Xebvs
  vZJnL => w肷ƍōȖ݂̂̃XebvsƂȂ.
  l̋L -> ͉\ȂׂĂ̂PXebvȖ񌋉ʂo͂邽ߕ
  ̌ʂo͂邱Ƃɒ.
  ȂŏɑΘbIɐi߂邩ǂ₢킹̂ s ܂ c ŉ
  邱. ŝ݂Ȃ s Ƃ݂Ȃ.

lambda> (\xsz.s(xs(s(xsz))))(\sz.s(sz)) =>
stepwise or continuously? s                s ܂͋sŃXebvsƂȂ
    \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 ̏ꍇ͑ΘbvZߒo
-> \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 ̌`Ŏw肷邱. [ ] := / Ȃǂ̋L̓_
  ł͎gȂߋʂł.

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)

_̎Rϐo
  _̎Rϐ@\ :print FV(_) ł.

lambda> :p FV(\xy.mx(ny))         :p  :print ̏ȗ`
{m, n}

_Z
  `ς݂̃}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]

̉Z
  `ς݂̃}N\ɂ :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?

ċA
  `ς݂̃}N\ɂ :macro(܂:m) ͂邱.

lambda> <Y><fact><3>;          Curry̕s_ZqgK
<6>
694 step(s) [0.858ms]
lambda> <Yt><fact><3>;         Turing̕s_ZqgK
<6>
709 step(s) [0.400ms]

pair -- car, cdr, cons
  `ς݂̃}N\ɂ :macro(܂:m) ͂邱.

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

Kp
  Ƃ
      (\mn.m+n)3 -> \n.3+n
  .  +  3 ȂǗL@gĂ邱Ƃɒ.
  Ӗ
      Qϐ֐ \mn.m+n RɕKpƂPϐ֐ \n.3+n ɂȂ
  Ƃ.

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

  ۂɂꂪɂRZ֐ƂȂĂ邱ƂmF邽߂
      (\n.3+n)2 -> 5
  ƂȂ邱Ƃ.

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

֐
  ֐ f  g ̊֐ \fgx.g(fx) ŕ\ł.
  ̓IȂQ̊֐
      add1 = <add><1> = (\mnsz.ms(nsz))(\sz.sz)    L@ \x.1+x
      mul2 = <mul><2> = (\mns.m(ns))(\sz.s(sz))      L@ \x.2*x
  ̊֐
      (\fgx.g(fx))<add1><mul2>                      L@ \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]

  ۂɂꂪOq̍֐ƂȂĂ邱ƂmF邽߂
      (\x.2*(1+x))5 -> 12
  ƂȂ邱Ƃ.

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

}N`
  }N`̃V^NX
      }N = _ ;
  ł.
  t@CɃ}N`LqĂꍇ͉L̕@Ń[hł.
    (1) :load R}hŎsɓǂݍ.
    (2) R}hs -l IvVŋNɓǂݍ.

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

lambda> :load macrofile     t@C}N`ǂݍ.

vZʂ̕\ύX
  ʂo͂ۂ :format R}hŕ\ύXł.
  :format R}ḧƂĉ\Ȓl͎̂Ƃ.
         abbrev łȌȐwI\   [] xy.xyz
         math   ȌȒʏ̐wI\ [] x.y.xyz
         proper ʂ̑wI\   [] x.(y.((xy)z))
   :reshape R}hŌʂ̕}Nɒu邩ǂ
  ł. ftHg̓}Nɒu.

lambda> :format proper
lambda> \xy.xyz;
\x.(\y.((xy)z))           ʂ߃_̍\mɂȂ.
0 step(s) [0.001ms]
lambda> :f math
lambda> \xy.xyz;
\x.\y.xyz                 _ۂPŕ\.
0 step(s) [0.000ms]
lambda> :f abbrev
lambda> \xy.xyz;
\xy.xyz                   ʏ͂̌`ŏo͂.
0 step(s) [0.000ms]

lambda> :reshape off      }NɒuȂݒ
lambda> <Y><fact><3>;
\sz.s(s(s(s(s(sz)))))      <6> Ӗ.
694 step(s) [0.762ms]
lambda> :r                }Nɒuݒ
lambda> <Y><fact><3>;
<6>                       ʂ`ς݃}NɒuĂ.
694 step(s) [0.761ms]

g[X
  :trace R}hŃg[Xo͂𐧌ł.
  g[Xo͂̐
    E->L͊Ȗ񌋉ʂ\.
    ECfǧ͕vZł邱Ƃ\.
    E--L͊Yϊ̋K\. (vZ_ q p.65)

lambda> :t              g[Xo͊Jn
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          g[Xo͒~
lambda> <succ><3>;
<4>
3 step(s) [0.000ms]

