Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
TaPL 7 章 型なしラムダ計算の1ステップ評価の OCaml による実装
(* Utilities *)
let (|>) x f = f x
let (|-) f g = fun x -> g (f x)
let getOrElse defVal = function
| Some(v) -> v
| None -> defVal
(* Term Definition *)
type term =
| TmVar of int * int (* 変数 : deBruijn_index * term_length *)
| TmAbs of string * term (* ラムダ抽象: bound_var_name * partial_term *)
| TmApp of term * term (* 関数適用 : arg_term * applying_term *)
| TmWrong (* 不正な項 (エラー処理用) *)
(* context: 特定のラムダ抽象における自由変数のリスト *)
type binding = NameBind
type context = (string * binding) list
(* context の長さはすなわちリストの長さ *)
let ctxlength = List.length
(* 特定の context での deBruijn インデックスから変数名を求める *)
let index2name ctx n =
if n < ctxlength ctx then
let name = List.nth ctx n |> fst in
Some(name)
else
None
(* 標準の List.find のオプション版 *)
let tryo f x = try Some(f x) with _ -> None
let listfind p = tryo (List.find p)
(* 現在の変数名を含む新しい context を作成して返す。
* 変数名が既に存在する場合は重複がなくなるまで ' をつけた変数名にする *)
let rec pickfreshname ctx name =
let oldname = listfind (fst |- ((=) name)) ctx in
match oldname with
| Some(name, _) -> pickfreshname ctx (name ^ "'")
| None -> let bind = (name, NameBind) in (bind::ctx, name)
(* 項の文字列表現。TaPL の printtm の純粋関数バージョン(単純に文字列を返す) *)
let rec string_of_term ctx = function
| TmVar(x, n) ->
if ctxlength ctx = n then
index2name ctx x |> getOrElse "[bad index]"
else
"[bad index]"
| TmAbs(name, tm) ->
let (ctx', name') = pickfreshname ctx name in
"(lambda " ^ name' ^ ". " ^ (string_of_term ctx' tm) ^ ")"
| TmApp(t1, t2) ->
"(" ^ (string_of_term ctx t1) ^ " " ^ (string_of_term ctx t2) ^ ")"
| TmWrong -> "[Wrong Evaluation]"
(* シフト演算。TaPL の定義 6.2.1 を書き起こしただけ
* ただし、シフトすると文脈の長さもシフトの分増える *)
let term_shift d t =
let rec walk c = function
| TmVar(x, ctxlen) when x < c -> TmVar(x, ctxlen+d)
| TmVar(x, ctxlen) -> TmVar(x+d, ctxlen+d)
| TmAbs(name, t) -> TmAbs(name, walk (c+1) t)
| TmApp(t1, t2) -> TmApp(walk c t1, walk c t2)
| TmWrong -> TmWrong
in walk 0 t
(* 代入。これも定義 6.2.4 とほとんど一緒 *)
let rec term_subst j s = function
| TmVar(k, _) when k = j -> s
| TmVar(_, _) as k -> k
| TmAbs(name, t) -> TmAbs(name, term_subst (j+1) (term_shift 1 s) t)
| TmApp(t1, t2) -> TmApp(term_subst j s t1, term_subst j s t2)
| TmWrong -> TmWrong
(* ベータ簡約。E-AppAbs 参照 *)
let term_subst_top s t =
let s' = term_shift 1 s in
let t' = term_subst 0 s' t in
term_shift (-1) t'
(* 値とはラムダ抽象のこと *)
let rec isval _ = function
| TmAbs(_, _) -> true
| _ -> false
(* 1 ステップ評価。図 5−3 参照
* 関数適用以外を評価しようとすると TmWrong になる *)
let rec eval1 ctx = function
| TmApp(TmAbs(_, t12), v2) when isval ctx v2 ->
term_subst_top v2 t12
| TmApp(v1, t2) when isval ctx v1 ->
let t2' = eval1 ctx t2 in
TmApp(v1, t2')
| TmApp(t1, t2) ->
let t1' = eval1 ctx t1 in
TmApp(t1', t2)
| _ -> TmWrong
(* 他ステップ評価。これ以上簡約できなくなるまで 1 ステップ評価を繰り返す *)
let rec eval ctx t =
let t' = eval1 ctx t in
match t' with
| TmWrong -> t
| _ -> eval ctx t'
(* テスト *)
let testcases = [
(* (λ x. x) λ y. y => λ y. y *)
(TmApp(TmAbs("x", TmVar(0, 1)), TmAbs("y", TmVar(0, 1))), TmAbs("y", TmVar(0, 1)));
(* (λ x. λ y. x) λ z. z => λ y. λ z. z *)
(TmApp(TmAbs("x", TmAbs("y", TmVar(1, 2))), TmAbs("z", TmVar(0, 1))), TmAbs("y", TmAbs("z", TmVar(0, 2))));
(* (λ x. λ x'. x) (λ x. x) => λ x'. λ x. x *)
(TmApp(TmAbs("x", TmAbs("x", TmVar(1, 2))), TmAbs("x", TmVar(0, 1))), TmAbs("x", TmAbs("x", TmVar(0, 2))));
(* (λ x. λ y. x) (λ z. z) (λ w. w) => (λ y. λ z. z) (λ w. w) *)
(TmApp(TmApp(TmAbs("x", TmAbs("y", TmVar(1, 2))), TmAbs("z", TmVar(0, 1))), TmAbs("w", TmVar(0, 1))),
TmApp(TmAbs("y", TmAbs("z", TmVar(0, 2))), TmAbs("w", TmVar(0, 1))));
(* (λ x. x) ((λ y. y) (λ z. z)) => (λ x. x) (λ z. z) *)
(TmApp(TmAbs("x", TmVar(0, 1)), TmApp(TmAbs("y", TmVar(0, 1)), TmAbs("z", TmVar(0, 1)))),
TmApp(TmAbs("x", TmVar(0, 1)), TmAbs("z", TmVar(0, 1))));
(* (λ x. x x) (λ x. x x) => (λ x. x x) (λ x. x x) *)
TmApp(TmAbs("x", TmApp(TmVar(0, 1), TmVar(0, 1))), TmAbs("x", TmApp(TmVar(0, 1), TmVar(0, 1)))),
TmApp(TmAbs("x", TmApp(TmVar(0, 1), TmVar(0, 1))), TmAbs("x", TmApp(TmVar(0, 1), TmVar(0, 1))));
] ;;
testcases
|> List.iteri (fun i -> fun (tsrc, texpect) ->
let tactual = eval1 [] tsrc in
let result = if (tactual = texpect) then "OK" else "**FAILURE**" in
Printf.printf "%d. %s\n => %s\n%s\n\n" (i+1) (string_of_term [] tsrc) (string_of_term [] tactual) result;
)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment