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"))))))