Skip to content

Instantly share code, notes, and snippets.

@nredjap
Last active Mar 22, 2020
Embed
What would you like to do?
TaPL7 UnTyped by Fsharp (Japanese comment)
open System
type Term =
// 名無し項 -> de Bruijnインデックス * 文脈全体の長さ(「デバッグのため、各変数ノードに対してもう一つ数を付け加え、一貫性検査を行うと有用である。付け加えた数は、その変数が現れる文脈全体の長さを常に保持するようにする」)
| TmVar of int * int
// 名付け項(ラムダ項?) -> 名前 * 項 (「項は内部的にはde Bruijnインデックスを使って表現されているが、これは明らかにユーザに提示すべき形ではない」~「各ラムダ抽象に束縛変数名のヒントとなる文字列を注記する」~「もしその文字列が現在の文脈においてすでに使われている名前と衝突するようならば、~衝突しない名前が見つかるまで、プライム記号(')を追加していく。」)
| TmAbs of String * Term
// 関数適用 -> 項1 * 項2
| TmApp of Term * Term
// 束縛自体は↓という全く自明な定義」(以降の章で拡充する)
type Binding = NameBind
// 「文脈型は、文字列とそれに関連付けられたbindingからなる組のリストである」
type Context = (String * Binding) list
// 「ctxLengthは文脈の長さを返す」
let ctxLength = List.length
// 「indexToNameは変数のインデックスから名前の文字列を引く」
let indexToName (ctx:Context) (t:int) =
match List.tryItem t ctx with
| Some(x) -> fst x
| None -> "[bad index]"
// 「pickFreshNameは文脈ctxとヒントの文字列xを受け取る。そしてxに似ているがctxに含まれていないx'を探し、そのx'をctxに加えて新たな文脈ctx'を作り、ctx'とx'を組として返す」
let rec pickFreshName ctx x =
let finded = List.tryFind (fun (str,_) -> str = x) ctx
match finded with
| Some(name, _) -> pickFreshName ctx (name + "'")
| None -> (ctx@[(x,NameBind)],x)
// 項の文字列表示
// ほぼ写経
let printTm ctx tm =
let rec tmToString ctx = function
| TmAbs(x,t1) ->
let (ctx',x') = pickFreshName ctx x
"" + x' + ". " + tmToString ctx' t1 + ")"
| TmApp(t1, t2) ->
"(" + tmToString ctx t1 + " " + tmToString ctx t2 + ")"
| TmVar(x, n) ->
if ctxLength ctx = n
then indexToName ctx x
else "[bad index]"
printfn "%s" <| tmToString ctx tm
// 「シフト定義(定義6.2.1)は、ほぼ一対一に記号を置き換えるだけ」
// ほぼ写経
let termShift d t =
let rec walk c = function
| TmVar(x, n) -> if x >= c then TmVar(x+d,n+d) else TmVar(x,n+d)
| TmAbs(x,t1) -> TmAbs(x,walk (c+1) t1)
| TmApp(t1,t2) -> TmApp(walk c t1, walk c t2)
walk 0 t
// 「代入関数も定義6.2.4からほぼ直接得られる」
// 項t中へのj番の変数への項sの代入`[j -> s]t`は、ここでは`termSubst j s t`となる。
// ほぼ写経
let termSubst j s t =
let rec walk c = function
| TmVar(x, n) -> if x = j + c then termShift c s else TmVar(x,n)
| TmAbs(x, t1) -> TmAbs(x, walk (c+1) t1)
| TmApp(t1,t2) -> TmApp(walk c t1, walk c t2)
walk 0 t
// 6.3評価 の(E-AppAbs)の操作をまとめた関数
// 「ラムダ計算の操作的意味論では、代入(と、その時のシフト)が使われる唯一の箇所はベータ簡約規則である」「以下の定義はこの一連のステップを一つにまとめたものである」
let termSubstTop s t = termShift (-1) (termSubst 0 (termShift 1 s) t)
// -- こっから[7.3評価]な --
// 「4章と同じく、評価関数は補助術後isValを用いる」
// ラムダ抽象かどうかの意味
let rec isVal ctx = function
| TmAbs(_) -> true
| _ -> false
exception NoRuleAppliesException
// 評価関数(1ステップ)
// 「項と一緒に文脈ctxを渡す点を除いて、評価規則をそのまま写したものになっている。この引数ctxは現段階のeval1関数では使っていないが、後により複雑な評価器の一部で必要となる」
// ほぼ写経
let rec eval1 ctx = function
| TmApp (TmAbs(x,t12),v2) when isVal ctx v2 ->
termSubstTop v2 t12
| TmApp(v1,t2) when isVal ctx v1 ->
TmApp(v1, eval1 ctx t2)
| TmApp(t1,t2) ->
TmApp(eval1 ctx t1, t2)
| _ ->
raise NoRuleAppliesException
// 多ステップ
let rec eval ctx t =
try
let t' = eval1 ctx t
eval ctx t'
with
| NoRuleAppliesException -> t
[<EntryPoint>]
let main argv =
let testTerms = [
// (lx.x) (ly.y) -> (ly.y)
TmApp(
TmAbs("x",TmVar(0,1)),
TmAbs("y",TmVar(0,1))
);
// (lx.y x z)(la.a) -> y (la.a) z // (l0.1 0 2)(l0.0) -> 0 (l0.0) 1のやつ
TmApp(
TmAbs("x", TmApp(TmApp(TmVar(1,1), TmVar(0,1)), TmVar(2,1))),
TmAbs("y", TmVar(0,1))
)
// たしかに自由変数は対応してない(BadIndex)
]
let testing t =
printTm [] t
printfn " after eval... ↓"
eval [] t |> printTm []
printfn ""
List.iter testing testTerms
printfn("Enterで終了します...")
Console.ReadLine() |> ignore
0 // return an integer exit code
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment