
Υ饹Ϸʤ׻Ԥ. ǽϤϼΤȤ.
    , ޥ, ޥ


  ϿŪɽȤ. ѿϱѻʸȤ. ޥ̾㳰.
  ȤxyϣĤѿxyǤϤʤؿxyŬѤ뤳Ȥɽ.
  ʸȾѥХåå(\)ޤѥ()ɽ.
  ʣϤθνλ("{0}", "{1}", "{2}")Ƿ׻򳫻Ϥ.
   [1] (\x.xx)e{0}
           νλꤹϤ.
           ξˤϴȽ׻֤¬.
   [2] (\y.y((\a.xa)(\a.a)))(\b.b){1}
           νλꤹȤ٤ƤΣƥå״̤Ϥ.
           ȤйήǧˤɬפʵǽǤ. ˴ˡ
           ˤߤȤʤ礬뤳ȤγǧˤȤ.
   [3] (\y.y((\a.xa)(\a.a)))(\b.b){2}
           νλꤹȺǺΣƥå״̤Ϥ.
           ׻Ū˿ʤ뤫ɤ䤤碌. Ūư
           ȤϷ׻򤹤٤ƽϤƤޤưǤ.
           νޤޤǷ֤ƺǽ̤ϤΤ
           [1]Ǥ.
   [4] \sz.s(nsz)[n:=\xy.x(xy)]{0} ޤ [\xy.x(xy)/n]\sz.s(nsz){0}
           ϥǤϤʤ黻ΰ̣Ǥ. 
           M[x:=N] ޤ [N/x]M ˤM,NϥǤxѿǤ.
 <>
    ׻̤ϦѴƤǽ. Ȥм׻̤  \y.y 
    ʤΤ \x.x ȽϤ뤳Ȥ.

ޥ
  ʣʥϤưפˤ뤿ޥǽǤ.
   (ޥȸƤͳñʤʸִǤ뤿.)
   [] true {3} \tf.t{0}
  ʣϤθλ({0})ǽ򳫻Ϥ.
  ޥλȤϥ {4}true{5} Τ褦˵Ҥ.
  ɽѤƤ뤿ѿΤ褦ʱѻʸȤϤʤ.

ޥɰ
  ޥɤϥޥȤϰۤʤϤǼ¹Ԥ򳫻Ϥ.
  ޥɤ϶̲ǽʬʸǤǧǽǤ.
{6}
     [1] βĶƤ׻ߤʤϷ׻Ǥڤ.
     [2] ǽʰ (̤Ǥʬʸ)
{7}

