Hatena::Groupcoders

ラシウラ出張所 このページをアンテナに追加 RSSフィード

2008/06/16

[]λ式のde Bruijn Index化と評価 λ式のde Bruijn Index化と評価 - ラシウラ出張所 を含むブックマーク はてなブックマーク - λ式のde Bruijn Index化と評価 - ラシウラ出張所 λ式のde Bruijn Index化と評価 - ラシウラ出張所 のブックマークコメント

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"

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

2007/05/11

[][] 関数の不動点  関数の不動点 - ラシウラ出張所 を含むブックマーク はてなブックマーク -  関数の不動点 - ラシウラ出張所  関数の不動点 - ラシウラ出張所 のブックマークコメント

OCaml:

type ('a, 'b) wrappedFun = Wrap of (('a, 'b) wrappedFun -> ('a -> 'b))

let fixpoint = fun funDef ->
  let unwrap = function Wrap(func) -> func in
  let genFunc = fun wrapped -> funDef (fun n -> (unwrap wrapped) wrapped n) in
  let wrapped = Wrap(genFunc) in
  genFunc wrapped

(* example *)
let factorial = fixpoint (fun fact n -> if n = 0 then 1 else n * fact (n - 1))

open Printf;;
printf "%d\n" (factorial 5)

Haskell:

fix f = f (fix f)

fact = fix $ \fn n -> if n < 1 then 1 else n * fn (n - 1)

main = do
    putStrLn $ show (fact 5)
    return ()

上のMLのようにhaskellで書くとghcでコンパイルがとまらなくなりました。

data Wrap a = Wrap ((Wrap a) -> a)

-- cannot compile, compiler infinit loop
fix f = genfunc wrapped
    where
      unwrap (Wrap g) = g
      genfunc wrapped = f ((unwrap wrapped) wrapped)
      wrapped = Wrap genfunc

fact = fix (\fact -> (\n -> if n == 0 then 1 else n * (fact (n - 1))))
main = putStrLn $ show (fact 10)