6

次の Shift/Reset チュートリアルを進めています: http://www.is.ocha.ac.jp/~asai/cw2011tutorial/main-e.pdf .

これまでのところ、 OchaCamlの例を Scalaに翻訳することでかなり良い結果が得られました (セクション 2.11 まで)。しかし今、私は壁にぶつかったようです。Asai/Kiselyov の論文のコードは、次の再帰関数を定義しています (これは OchaCaml だと思います)。

(* a_normal : term_t => term_t *)
let rec a_normal term = match term with
    Var (x) -> Var (x)
  | Lam (x, t) -> Lam (x, reset (fun () -> a_normal t))
  | App (t1, t2) ->
      shift (fun k ->
        let t = gensym () in (* generate fresh variable *)
        App (Lam (t, (* let expression *)
                  k (Var (t))), (* continue with new variable *)
             App (a_normal t1, a_normal t2))) ;;

この関数は、ラムダ式を A 正規化することになっています。これは私のScala翻訳です：

// section 2.11
object ShiftReset extends App {

  sealed trait Term
  case class Var(x: String) extends Term
  case class Lam(x: String, t: Term) extends Term
  case class App(t1: Term, t2: Term) extends Term

  val gensym = {
    var i = 0
    () => { i += 1; "t" + i }
  }

  def a_normal(t: Term): Term@cps[Term] = t match {
    case Var(x) => Var(x)
    case Lam(x, t) => Lam(x, reset(a_normal(t)))
    case App(t1, t2) => shift{ (k:Term=>Term) =>
      val t = gensym()
      val u = Lam(t, k(Var(t)))
      val v = App(a_normal(t1), a_normal(t2))
      App(u, v): Term
    }
  }

}

次のコンパイル エラーが発生します。

 found   : ShiftReset.Term @scala.util.continuations.cpsSynth 
             @scala.util.continuations.cpsParam[ShiftReset.Term,ShiftReset.Term]
 required: ShiftReset.Term
    case App(t1, t2) => shift{ (k:Term=>Term) =>
                                              ^
one error found

プラグインは、ネストされたものを処理できないと言っていると思いますshift...コードをコンパイルする方法はありますか(私が見落とした基本的なエラーまたはいくつかの回避策)? パターン マッチを if/else if/else に変換し、さらにローカル変数を導入しようとしましたが、同じエラーが発生しました。

代わりに、Haskell と Cont モナド (+ここからのシフト/リセット) を使用すると、より多くの運が得られるでしょうか? または、ネストされたシフトで同じタイプの制限が発生するでしょうか? チュートリアルの残りの部分を進めるために Haskell に切り替えてもかまわないので、Haskell タグも追加します。

編集：継続プラグインが処理できなかった行とそれを微調整する方法を見つけたJamesのおかげで、現在は機能しています。彼の回答のバージョンと次の書式設定コードを使用します。

def format(t: Term): String = t match {
  case Var(x) => s"$x"
  case Lam(x, t) => s"\\$x.${format(t)}"
  case App(Lam(x, t1), t2) => s"let $x = ${format(t2)} in ${format(t1)}"
  case App(Var(x), Var(y)) => s"$x$y"
  case App(Var(x), t2) => s"$x (${format(t2)})"
  case App(t1, t2) => s"(${format(t1)}) (${format(t2)})"
}

論文に記載されている出力を取得します（ただし、継続が実際にそれをどのように管理するかはまだわかりません）：

sCombinator:
\x.\y.\z.(xz) (yz)
reset{a_normal(sCombinator)}:
\x.\y.\z.let t1 = xz in let t2 = yz in let t3 = t1t2 in t3
4

1 に答える 1