ラムダ計算のインタープリタを作ったが、作りっぱなしでは面白くないので、A Tutorial Introduction to the Lambda Calculus をネタにラムダ計算によるプログラムをいろいろ試してみることにする。読解形式にはしないで、気ままにラムダ計算のプログラムを引用してラムダ計算機で実験していく。 ラムダ計算は「世界で最小の汎用プログラム言語」と呼ばれているようだが、すぐに思いつくのは次のような identity function くらいしかない。これは、単に引数を一つ取り、それを戻り値として返すだけだから何の面白みもない。 $ runghc Lambda.hs lambda> (lx.x) (lx.x) lambda> ((lx.x) a) a ラムダ計算機ではこのように β 簡約を自動でできるが、ラムダ式の入力は括弧を省略しない形式でないとできない。したがって、参考書に出てくる括弧を省略した、λxy.MNL は (lx.(ly.((M N) L) というように括弧を補充する必要がある。 ラムダ計算では論理の真理値を定義できる。論理値の true と false は次のように定義される。 true = λxy.x false = λxy.y ラムダ計算機では (= var term) 式で変数 var にラムダ式 term を束縛できる。変数名は alphaNum なので数字と英数字の文字列になる。数字だけの変数にすることもできる。 lambda> (= true (lx.(ly.x))) lambda> (= false (lx.(ly.y))) lambda> true (lx.(ly.x)) lambda> false (lx.(ly.y)) true は引数 x y をとり、第1引数 x を返す関数だ。false は引数 x y をとり y を返す。 lambda> ((true a) b) a lambda> ((false a) b) b なぜこれが true と false なのだろうと不思議に感じるが、true と false がこのように定義されていると、if c then a else b という if ~ then ~ else 式が次のように簡単に定義できる。 if = λcxy.cxy lambda> (=if (lc.(lx.(ly.((c x) y))))) lambda> (((if true) a) b) a lambda> (((if false) a) b) b これでラムダ計算機もめでたく、条件分岐を記述できるようになった。 論理値が導入できたので論理記号も定義したい。NOT は次のように定義できる。 NOT = λx.xFT true と false の別名 T と F を作って上の NOT を実装してみる。 lambda> (= T true) lambda> (= F false) lambda> (= NOT (lx.((x F) T))) lambda> (NOT true) (lx.(ly.y)) ..... false lambda> (NOT false) (lx.(ly.x)) ..... true AND と OR の定義は次のようになる。 AND = λxy.xyF OR = λxy.xTy lambda> (= AND (lx.(ly.((x y) F)))) lambda> ((AND true) false) (lx.(ly.y)) lambda> ((AND true) true) (lx.(ly.x)) lambda> (= OR (lx.(ly.((x T) y)))) lambda> ((OR true) false) (lx.(ly.x)) lambda> ((OR false) false) (lx.(ly.y)) 含意の定義は次のようになる。 lambda> (= IMPLY (lx.(ly.((OR (NOT x)) y)))) lambda> ((IMPLY true) true) (lx.(ly.x)) lambda> ((IMPLY true) false) (lx.(ly.y)) ラムダ計算機もだんだんプログラム言語らしくなってきた。一見不可解な true と false の定義で条件分岐や論理演算が定義できるのが面白い。 ラムダ計算機を使っていると、はるか昔にマイコンに機械語のプログラムを打ち込んでLEDを点滅させて感動していたときのことが思い出される。ラムダ計算の理論的なことは置いておいても、ラムダ計算機をいじるのは楽しい。
by tnomura9
| 2019-09-08 07:26
| Haskell
|
Comments(0)
|
カテゴリ
新型コロナウイルス 主インデックス Haskell 記事リスト 圏論記事リスト 考えるということのリスト 考えるということ ラッセルのパラドックス Haskell Prelude Ocaml ボーカロイド 圏論 jQuery デモ HTML Python ツールボックス XAMPP Ruby ubuntu WordPress 脳の話 話のネタ リンク 幸福論 キリスト教 心の話 メモ 電子カルテ Dojo JavaScript C# NetWalker ed と sed HTML Raspberry Pi C 言語 命題論理 以前の記事
最新のトラックバック
最新のコメント
ファン
記事ランキング
ブログジャンル
画像一覧
|
ファン申請 |
||