情報システム科学I

lambda.jarの使い方

2009年度冬学期 担当: 増原英彦

以下では lambda 計算インタプリタの実行方法を説明します。 ここでは教育用計算機システムのiMac環境で実行することを前提にしています。
  1. まず lambda 計算インタプリタ lambda.jar を自分のホームディレクトリにダウンロードします。
  2. 「Terminal」アプリケーションを起動し、lambda.jar をダウンロードしたディレクトリに移動します。
  3. 現在のディレクトリにlambda.jarがあることを確認します。下の「ls -l lambda.jar」を入力して下のような表示が出れば大丈夫です。(ca12345$ という部分はログインしている機械によって変わります。また、所有者名・グループ名・サイズ・更新時刻は違うかも知れません。)
    ca12345$ ls -l lambda.jar
    合計 1
    -rw------- 1 masuhara teacher 8073 11 25 18:42 lambda.jar
    ca12345$
  4. インタプリタを実行します。下の「java -jar lambda.jar」を入力すると、「>」が表示されます。この状態でλ項を入力すると簡約した結果を表示します。
    ca12345$ java -jar lambda.jar
    > \x.x
    (\x.x)
    > (\x.x)y
    ((\x.x)y)
    y
    > S=\nfx.f(nfx)
    (\nfx.f(nfx))
    > Z0=\fx.x
    (\fx.x)
    > Z1=SZ0
    ((\nfx.f(nfx))(\fx.x))
    (\fx.f((\fx.x)fx))
    (\fx.f((\x.x)x))
    (\fx.fx)
    λのかわりに\を使います。
    この式は(λx.(x))を意味します。
    式が表示されます。
    この式は((λx.(x))y)を意味します。
    入力された式と
    簡約した結果が表示されます。
    「変数=式」を入力すると、
    式を覚させることができます。
    変数名はアルファベット1文字に
    数字を0個以上続けたものです。
    簡約した結果を変数に
    覚えることもできます。
    > Z2=S Z1
    ((\nfx.f(nfx))(\fx.fx))
    (\fx.f((\fx.fx)fx))
    (\fx.f((\x.fx)x))
    (\fx.f(fx))
    		 この例は Z1 (1) の S (successor) を
    Z2 と定義しています。
    > A=\nmfx.mf(nfx)
    (\nmfx.mf(nfx))
    > A Z2 Z1
    ((\nmfx.mf(nfx))(\fx.f(fx))(\fx.fx))
    ((\mfx.mf((\fx.f(fx))fx))(\fx.fx))
    (\fx.(\fx.fx)f((\fx.f(fx))fx))
    (\fx.(\x.fx)((\fx.f(fx))fx))
    (\fx.f((\fx.f(fx))fx))
    (\fx.f((\x.f(fx))x))
    		 A(足し算)を定義して

    2+1を計算させます
    (\fx.f(f(fx)))
    > Z2 (A Z2) Z2
    ((\fx.f(fx))((\nmfx.mf(nfx))(\fx.f(fx)))...
    ((\x.(\nmfx.mf(nfx))(\fx.f(fx))((\nmfx.m...
    ((\nmfx.mf(nfx))(\fx.f(fx))((\nmfx.mf(nf...
    ((\mfx.mf((\fx.f(fx))fx))((\nmfx.mf(nfx)...
    (\fx.(\nmfx.mf(nfx))(\fx.f(fx))(\fx.f(fx...
    (\fx.(\mfx.mf((\fx.f(fx))fx))(\fx.f(fx))...
    (\fx.(\fx.(\fx.f(fx))f((\fx.f(fx))fx))f(...
    (\fx.(\x.(\fx.f(fx))f((\fx.f(fx))fx))((\...
    (\fx.(\fx.f(fx))f((\fx.f(fx))f((\fx.f(fx...
    (\fx.(\x.f(fx))((\fx.f(fx))f((\fx.f(fx))...
    (\fx.f(f((\fx.f(fx))f((\fx.f(fx))fx))))
    (\fx.f(f((\x.f(fx))((\fx.f(fx))fx))))
    		 確かに3になっています
    もっと複雑な項を簡約すると

    (本当はもっと長い式が
    表示されます)
    Continue? [return]
    (\fx.f(f(f(f((\fx.f(fx))fx)))))
    (\fx.f(f(f(f((\x.f(fx))x)))))
    (\fx.f(f(f(f(f(fx))))))
    > #
    > S (S Z0)
    ((\nfx.f(nfx))((\nfx.f(nfx))(\fx.x)))
       0             1
    Redex?1
    ((\nfx.f(nfx))(\fx.f((\fx.x)fx)))
       0                   1
    Redex?1
    ((\nfx.f(nfx))(\fx.f((\x.x)x)))
       0                   1
    Redex?1
    ((\nfx.f(nfx))(\fx.fx))
       0
    		 途中で続けるかどうかを
    聞かれます。enterを入力すると
    簡約を続けます。nと入力すると
    そこで停止します。
    #を入力すると、手で簡約する場所を
    指定できるようになります。
    λ抽象された変数名の下に
    書かれた数が簡約の場所を
    表わしますので、
    番号で指示します。
    Redex?
    (\fx.f((\fx.fx)fx))
             0
    Redex?
    (\fx.f((\x.fx)x))
             0
    Redex?
    (\fx.f(fx))

    > #
    		 単にenterを入力すると
    0番を簡約します。
    > S (S Z0)
    ((\nfx.f(nfx))((\nfx.f(nfx))(\fx.x)))
    (\fx.f((\nfx.f(nfx))(\fx.x)fx))
    (\fx.f((\fx.f((\fx.x)fx))fx))
    (\fx.f((\x.f((\fx.x)fx))x))
    (\fx.f(f((\fx.x)fx)))
    (\fx.f(f((\x.x)x)))
    (\fx.f(fx))
    >
    		もう一度#を入力すると
    自動的な簡約に戻ります。
    Hidehiko Masuhara, December 2009