ラムダ計算を実装してみる
まず、OCaml版のラムダ計算があればうれしいので、ラムダ計算入門 *1 を参考に、TAPLのソースにあわせる形で、Scalaに書き換えてみました。
package _01lambda trait Term // λ式を表すデータ型 case class TmVar(s:String) extends Term // 変数 // 変数名は文字列であらわすことにする case class TmAbs(s:String,e:Term) extends Term // λ抽象 case class TmApp(e1:Term, e2:Term) extends Term // 関数適用 class NoRuleApplies(t: Term) extends Exception("No rule applies for term: " + t) object Demo { var counter = 0 // 整数0を持った参照セルcounterを作る // 新しい変数名を作る補助的な関数 def gensym():String = { counter += 1 // counter の中身を一つ増やす "g" + counter // g1, g2, g3, ... 等の文字列を返す } // ((lambda x e1) e2)を評価するために、e1のxをe2に書き換える。 def subst(e2:Term, x:String, e1:Term):Term = { e1 match { // e1が 変数のとき case TmVar(y) => // 変数名が同じなら置き換え、同じでなければそのまま if (x == y) e2 else TmVar(y) // ラムダ抽象のとき ((lambda x (lambda y e)) e2) => eのyをy1に置き換えて、xをe2に置き換え、たものをe'として // 結果、(lambda y1 e') case TmAbs(y, e) => // 新しい識別子を作って val y1 = gensym() // その値で、y TmVar(y1) TmAbs(y1, subst(e2, x, subst(TmVar(y1), y, e))) // 関数適用のときは、内部を置き換える。 case TmApp(e, e1) => TmApp(subst(e2, x, e), subst(e2, x, e1)) } } // e を受け取り、e => e' となる e' のリストを返す def eval1(t:Term):Term = { t match { case TmApp(TmAbs(x, e0), e2) if (isVal(e2)) => subst(e2, x, e0) case TmApp(e1, e2) if (isVal(e1)) => TmApp(eval1(e1), e2) case TmApp(e1, e2) => TmApp(e1, eval1(e2)) case _ => throw new NoRuleApplies(t) } } // 簡約できなくなるまで eval1 を反復する def eval(t:Term):Term = { try { val t1 = eval1(t) eval(t1) } catch { case _: NoRuleApplies => t } } // def isVal(t: Term): Boolean = { t match { case TmAbs(_, _) => true case TmVar(_) => true case _ => false } } // def main(args:Array[String]) { val cmds = List[Term]( TmVar("x"), TmApp(TmApp(TmVar("x"),TmVar("x")),TmVar("x")), // (λ x. x) TmAbs("x", TmVar("x")), // (λ x. x) (λ x. x) TmApp(TmAbs("x", TmVar("x")), TmAbs("x", TmVar("x"))), // ((λx. x) (λx. x)) ((λx. x) (λx. x)) TmApp( TmApp(TmAbs("x", TmVar("x")), TmAbs("x", TmVar("x"))), TmApp(TmAbs("x", TmVar("x")), TmAbs("x", TmVar("x")))), TmApp(TmAbs("x", TmVar("x")),TmVar("x")), TmApp(TmAbs("x", TmVar("x")),TmVar("y")) ) cmds.foreach { case e => println(e) println("|") println("V") val e2 = eval(e) println(e2) } } }
TAPLの内容に若干近づけてみましたが、de bruijn index は使ってなくて、環境もありません。 ここに、TAPLのarithの構文木とその処理をまず追加してみます。
case object TmTrue extends Term case object TmFalse extends Term case class TmIf(cond: Term, t1: Term, t2: Term) extends Term case object TmZero extends Term case class TmSucc(t: Term) extends Term case class TmPred(t: Term) extends Term case class TmIsZero(t: Term) extends Term
でしばらく弄ってみました。
次に、レコード操作の構文木と処理を入れて弄ってみます。
case class TmRecord(fields: List[(String, Term)]) extends Term case class TmProj(t: Term, proj: String) extends Term
次は文字列の構文木とその処理を入れてみます。殆ど、処理はないんですね。 インタプリタだと楽だなぁ。
最後に、letの構文木と処理を入れて弄ってみます。
case class TmLet(l: String, t1: Term, t2: Term) extends Term
と言う事をやってみた結果のソースが以下になります。
package _01lambda2 trait Term // λ式を表すデータ型 case class TmVar(s:String) extends Term // 変数 // 変数名は文字列であらわすことにする case class TmAbs(s:String,e:Term) extends Term // λ抽象 case class TmApp(e1:Term, e2:Term) extends Term // 関数適用 case object TmTrue extends Term case object TmFalse extends Term case class TmIf(cond: Term, t1: Term, t2: Term) extends Term case object TmZero extends Term case class TmSucc(t: Term) extends Term case class TmPred(t: Term) extends Term case class TmIsZero(t: Term) extends Term case class TmRecord(fields: List[(String, Term)]) extends Term case class TmProj(t: Term, proj: String) extends Term case class TmString(s: String) extends Term case class TmLet(l: String, t1: Term, t2: Term) extends Term class NoRuleApplies(t: Term) extends Exception("No rule applies for term: " + t) object Demo { var counter = 0 // 整数0を持った参照セルcounterを作る // 新しい変数名を作る補助的な関数 def gensym():String = { counter += 1 // counter の中身を一つ増やす "g" + counter // g1, g2, g3, ... 等の文字列を返す } // ((lambda x e1) e2)を評価するために、e1のxをe2に書き換える。 def subst(e2:Term, x:String, e1:Term):Term = { e1 match { // e1が 変数のとき case TmVar(y) => // 変数名が同じなら置き換え、同じでなければそのまま if (x == y) e2 else TmVar(y) // ラムダ抽象のとき ((lambda x (lambda y e)) e2) => eのyをy1に置き換えて、xをe2に置き換え、たものをe'として // 結果、(lambda y1 e') case TmAbs(y, e) => // 新しい識別子を作って val y1 = gensym() // その値で、y TmVar(y1) TmAbs(y1, subst(e2, x, subst(TmVar(y1), y, e))) // 関数適用のときは、内部を置き換える。 case TmApp(e, e1) => TmApp(subst(e2, x, e), subst(e2, x, e1)) case TmTrue => TmTrue case TmFalse => TmFalse case TmIf(t1, t2, t3) => TmIf(subst(e2, x, t1), subst(e2, x, t2), subst(e2, x, t3)) case TmZero => TmZero case TmSucc(t1) => TmSucc(subst(e2, x, t1)) case TmPred(t1) => TmPred(subst(e2, x, t1)) case TmIsZero(t1) => TmIsZero(subst(e2, x, t1)) case TmProj(t1, l) => TmProj(subst(e2, x, t1), l) case TmRecord(fields) => TmRecord(fields.map { case (l, t) => (l, subst(e2, x, t)) }) case t: TmString => t case TmLet(y, t1, t2) => val y1 = gensym() TmLet(y1, subst(e2, x, t1), subst(e2, x, subst(TmVar(y1), y, t2))) } } // e を受け取り、e => e' となる e' のリストを返す def eval1(t:Term):Term = { t match { case TmApp(TmAbs(x, e0), e2) if (isVal(e2)) => subst(e2, x, e0) case TmApp(e1, e2) if (isVal(e1)) => TmApp(e1, eval1(e2)) case TmApp(e1, e2) => TmApp(eval1(e1), e2) case TmIf(TmTrue, t2, t3) => t2 case TmIf(TmFalse, t2, t3) => t3 case TmIf(t1, t2, t3) => TmIf(eval1(t1), t2, t3) case TmSucc(t1) => TmSucc(eval1(t1)) case TmPred(TmZero) => TmZero case TmPred(TmSucc(nv1)) if (isNumericVal(nv1)) => nv1 case TmPred(t1) => TmPred(eval1(t1)) case TmIsZero(TmZero) => TmTrue case TmIsZero(TmSucc(nv1)) if (isNumericVal(nv1)) => TmFalse case TmIsZero(t1) => TmIsZero(eval(t1)) case TmRecord(fields) => def evalAField(l: List[(String, Term)]): List[(String, Term)] = l match { case Nil => throw new NoRuleApplies(t) case (l, v1) :: rest if isVal(v1) => (l, v1) :: evalAField(rest) case (l, t1) :: rest => (l, eval1(t1)) :: rest } TmRecord(evalAField(fields)) case TmProj(v1 @ TmRecord(fields), l) if isVal(v1) => fields.find { _._1 == l } match { case Some((_, ti)) => ti case None => throw new NoRuleApplies(t) } case TmProj(t1, l) => TmProj(eval1(t1), l) case TmLet(x, v1, t2) if isVal(v1) => subst(v1, x, t2) case TmLet(x, v1, t2) => TmLet(x, eval(v1), t2) case _ => throw new NoRuleApplies(t) } } // 簡約できなくなるまで eval1 を反復する def eval(t:Term):Term = { try { val t1 = eval1(t) eval(t1) } catch { case _: NoRuleApplies => t } } // def isNumericVal(t: Term): Boolean = { t match { case TmZero => true case TmSucc(t) => isNumericVal(t) case _ => false } } // def isVal(t: Term): Boolean = { t match { case TmAbs(_, _) => true case TmVar(_) => true case TmTrue => true case TmFalse => true case t if (isNumericVal(t)) => true case TmRecord(fields) => fields.forall { case (_, ti) => isVal(ti) } case TmString(_) => true case _ => false } } // def main(args:Array[String]) { val cmds = List[Term]( TmVar("x"), TmApp(TmApp(TmVar("x"),TmVar("x")),TmVar("x")), // (λ x. x) TmAbs("x", TmVar("x")), // (λ x. x) (λ x. x) TmApp(TmAbs("x", TmVar("x")), TmAbs("x", TmVar("x"))), // ((λx. x) (λx. x)) ((λx. x) (λx. x)) TmApp( TmApp(TmAbs("x", TmVar("x")), TmAbs("x", TmVar("x"))), TmApp(TmAbs("x", TmVar("x")), TmAbs("x", TmVar("x")))), // TmApp(TmAbs("x", TmVar("x")),TmVar("x")), TmApp(TmAbs("x", TmVar("x")),TmVar("y")), TmZero, TmTrue, TmFalse, TmIsZero(TmZero), TmIsZero(TmSucc(TmZero)), TmIsZero(TmPred(TmSucc(TmZero))), TmProj(TmRecord(List("a"->TmZero,"b"->TmZero)),"b"), TmString("mojirtu"), TmApp(TmAbs("x", TmString("mojiretu")),TmVar("y")), TmApp(TmApp(TmAbs("x",TmAbs("y",TmApp(TmVar("x"),TmVar("y")))),TmZero),TmSucc(TmZero)), TmLet("x",TmString("X"),TmVar("x")) ) cmds.foreach { case e => println(e) println("|") println("V") val e2 = eval(e) println(e2) } } }
こういうソースを書く事で、untypedの実装について詳しくなる事が出来ました。 ブールとペアノ数、レコード、文字列、letが追加されています。
次はここに、Mapを使った環境を入れてみようと思います。 この辺は、何度もいろいろ実装してみる事で理解が深まるんじゃないかと思います。
TAPLの実装では、substでの再帰処理は、実は似たような操作を複数書く為に、 tmMapと言う関数にビジターパターンを作るような感じで書いてあります。 高階関数を使う事でスッキリする例ですね。
マクロで書かれていた物のうちで、高階関数を使えばマクロを使わなくてすむ処理は 結構あるように思います。
自分の場合は、とにかく、ラムダ計算の実装になれる事を目標にしているので、 de bruijn indexを使わないでsimpleboolの実装をしてみたいと思います。
簡単な実装になれてしまえば、難しい実装も簡単に見えるはずです。 そして、実装が分かっていれば、理論もまた飲み込みやすいはずです。
