de Bruijn index
簡約時のα変換不要にするラムダ式の変数表現法
- λx.λy.x → λ λ 2
- λu.λv.((λx.λy.x) u v) → λλ((λλ2) 2 1)
- => λλ((λ3) 1) => λλ2
その式の内側から数えたλのインデックスで変数名を表現する。
β変換では
- 適用する関数からのλの数と同じになる変数が置換対象
- 各置換対象変数ごとに
- その置換対象の変数のIndexをnとする
- 置き換わる側の式内の自由変数はすべて+nして、その置換対象変数と入れ替える
- λをはずし本体内の自由変数はすべて-1する
アルファ変換が必要ないというよりは、アルファ変換を組み込んだ簡約になっている。
evaluator例
data Term = Var Int | App Term Term | Lam Term | Con String deriving Show eval :: Term -> Term eval (Var n) = Var n eval (Con s) = Con s eval (Lam b) = Lam b eval (App (Lam b) opd) = eval (replace 0 b (eval opd)) eval (App opr opd) = eval (App (eval opr) opd) replace :: Int -> Term -> Term -> Term replace var (Lam b) arg = Lam (replace (var+1) b arg) replace var (App opr opd) arg = App (replace var opr arg) (replace var opd arg) replace var (Con s) arg = Con s replace var (Var n) arg | n < var = Var n replace var (Var n) arg | n == var = fixfree 0 var arg replace var (Var n) arg | n > var = Var (n-1) fixfree :: Int -> Int -> Term -> Term fixfree depth var (Lam b) = Lam (fixfree (depth+1) var b) fixfree depth var (App opr opd) = App (fixfree depth var opr) (fixfree depth var opd) fixfree depth var (Con s) = Con s fixfree depth var (Var n) | n <= depth = Var n fixfree depth var (Var n) | n > depth = Var (n+var-1) -- examples icomb = Lam (Var 0) kcomb = Lam (Lam (Var 1)) scomb = Lam (Lam (Lam (App (App (Var 2) (Var 0)) (App (Var 1) (Var 0))))) bcomb = Lam (Lam (Lam (App (Var 2) (App (Var 1) (Var 0))))) ccomb = Lam (Lam (Lam (App (App (Var 2) (Var 0)) (Var 1)))) ycomb = Lam (App (Lam (App (Var 1) (App (Var 0) (Var 0)))) (Lam (App (Var 1) (App (Var 0) (Var 0))))) -- eval (App (App (App scomb kcomb) kcomb) (Con "a")) => Con "a"
Lambda式ASTをde Bruijn Index項に変換
data Expr = V String | A Expr Expr | L String Expr | C String deriving Show compile :: [String] -> Expr -> Term compile namestack (C s) = Con s compile namestack (A opr opd) = App (compile namestack opr) (compile namestack opd) compile namestack (L p b) = Lam (compile (p:namestack) b) compile namestack (V v) = Var (find 0 v namestack) where find index var (name:rest) = if var == name then index else find (index+1) var rest -- compile [] (L "x" (L "y" (V "x"))) => Lam (Lam (Var 1)) -- compile [] (L "f" (A (L "x" (A (V "f") (A (V "x") (V "x")))) (L "x" (A (V "f") (A (V "x") (V "x"))))))