interpretować PARIGOT jest lambda-MU rachunku w Haskell

Question

Można zinterpretować rachunek lambda w Haskell:

data Expr = Var String | Lam String Expr | App Expr Expr 

data Value a = V a | F (Value a -> Value a) 

interpret :: [(String, Value a)] -> Expr -> Value a 
interpret env (Var x) = case lookup x env of 
    Nothing -> error "undefined variable" 
    Just v -> v 
interpret env (Lam x e) = F (\v -> interpret ((x, v):env) e) 
interpret env (App e1 e2) = case interpret env e1 of 
    V _ -> error "not a function" 
    F f -> f (interpret env e2) 

Jak można powyższe interpreter zostać rozszerzony na lambda-mu calculus? Domyślam się, że powinien on wykorzystywać kontynuacje do interpretacji dodatkowych konstrukcji w tym rachunku. (15) i (16) z Bernardi&Moortgat paper są tego rodzaju tłumaczeniami, jakich oczekuję.

Jest to możliwe, ponieważ Haskell to Turing-complete, ale w jaki sposób?

Podpowiedź: Zobacz komentarz na stronie 197 o this research paper dla intuicyjnego znaczenia segregatora mu.

Answer 1

Uwaga: to tylko częściowa odpowiedź, ponieważ nie jestem pewien, jak rozszerzyć interpreter.

Wydaje się, że jest to dobry przypadek użycia dla DataKinds. Typ danych Expr jest indeksowany na typie nazwanym lub nienazwanym. Zwykłe konstrukcje lambda generują tylko nazwane terminy.

{-# LANGUAGE GADTs, DataKinds, KindSignatures #-} 

data TermType = Named | Unnamed 

type Var = String 
type MuVar = String 

data Expr (n :: TermType) where 
    Var :: Var -> Expr Unnamed 
    Lam :: Var -> Expr Unnamed -> Expr Unnamed 
    App :: Expr Unnamed -> Expr Unnamed -> Expr Unnamed 

i dodatkowy Mu i Name konstrukty mogą manipulować TermType.

... 
    Name :: MuVar -> Expr Unnamed -> Expr Named 
    Mu :: MuVar -> Expr Named -> Expr Unnamed 

Answer 2

Oto bezmyślne transliteracji zasad redukcji z papieru, z wykorzystaniem reprezentacji @ user2407038 (jak zobaczysz, kiedy mówię, bezmyślne, ja naprawdę mam na myśli bezmyślne):

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-} 
{-# LANGUAGE StandaloneDeriving #-} 

import Control.Monad.Writer 
import Control.Applicative 
import Data.Monoid 

data TermType = Named | Unnamed 

type Var = String 
type MuVar = String 

data Expr (n :: TermType) where 
    Var :: Var -> Expr Unnamed 
    Lam :: Var -> Expr Unnamed -> Expr Unnamed 
    App :: Expr Unnamed -> Expr Unnamed -> Expr Unnamed 
    Freeze :: MuVar -> Expr Unnamed -> Expr Named 
    Mu :: MuVar -> Expr Named -> Expr Unnamed 
deriving instance Show (Expr n) 

substU :: Var -> Expr Unnamed -> Expr n -> Expr n 
substU x e = go 
    where 
    go :: Expr n -> Expr n 
    go (Var y) = if y == x then e else Var y 
    go (Lam y e) = Lam y $ if y == x then e else go e 
    go (App f e) = App (go f) (go e) 
    go (Freeze alpha e) = Freeze alpha (go e) 
    go (Mu alpha u) = Mu alpha (go u) 

renameN :: MuVar -> MuVar -> Expr n -> Expr n 
renameN beta alpha = go 
    where 
    go :: Expr n -> Expr n 
    go (Var x) = Var x 
    go (Lam x e) = Lam x (go e) 
    go (App f e) = App (go f) (go e) 
    go (Freeze gamma e) = Freeze (if gamma == beta then alpha else gamma) (go e) 
    go (Mu gamma u) = Mu gamma $ if gamma == beta then u else go u 

appN :: MuVar -> Expr Unnamed -> Expr n -> Expr n 
appN beta v = go 
    where 
    go :: Expr n -> Expr n 
    go (Var x) = Var x 
    go (Lam x e) = Lam x (go e) 
    go (App f e) = App (go f) (go e) 
    go (Freeze alpha w) = Freeze alpha $ if alpha == beta then App (go w) v else go w 
    go (Mu alpha u) = Mu alpha $ if alpha /= beta then go u else u 

reduceTo :: a -> Writer Any a 
reduceTo x = tell (Any True) >> return x 

reduce0 :: Expr n -> Writer Any (Expr n) 
reduce0 (App (Lam x u) v) = reduceTo $ substU x v u 
reduce0 (App (Mu beta u) v) = reduceTo $ Mu beta $ appN beta v u 
reduce0 (Freeze alpha (Mu beta u)) = reduceTo $ renameN beta alpha u 
reduce0 e = return e 

reduce1 :: Expr n -> Writer Any (Expr n) 
reduce1 (Var x) = return $ Var x 
reduce1 (Lam x e) = reduce0 =<< (Lam x <$> reduce1 e) 
reduce1 (App f e) = reduce0 =<< (App <$> reduce1 f <*> reduce1 e) 
reduce1 (Freeze alpha e) = reduce0 =<< (Freeze alpha <$> reduce1 e) 
reduce1 (Mu alpha u) = reduce0 =<< (Mu alpha <$> reduce1 u) 

reduce :: Expr n -> Expr n 
reduce e = case runWriter (reduce1 e) of 
    (e', Any changed) -> if changed then reduce e' else e 

To „pracuje” na przykład z papieru: z

example 0 = App (App t (Var "x")) (Var "y") 
    where 
    t = Lam "x" $ Lam "y" $ Mu "delta" $ Freeze "phi" $ App (Var "x") (Var "y") 
example n = App (example (n-1)) (Var ("z_" ++ show n)) 

mogę zmniejszyć example n do oczekiwanego rezultatu:

*Main> reduce (example 10) 
Mu "delta" (Freeze "phi" (App (Var "x") (Var "y"))) 

Powodem, dla którego umieszczam przerażające cytaty wokół "prac" powyżej jest to, że nie mam intuicji co do rachunku λμ, więc nie wiem, co powinienem zrobić.

Answer 3

Co powiesz na coś podobnego poniżej. Nie mam dobrego pomysłu na przechodzenie przez Value a, ale przynajmniej widzę, że ocenia on example n na MuV.

import Data.Maybe 

type Var = String 
type MuVar = String 

data Expr = Var Var 
      | Lam Var Expr 
      | App Expr Expr 
      | Mu MuVar MuVar Expr 
      deriving Show 

data Value a = ConV a 
      | LamV (Value a -> Value a) 
      | MuV (Value a -> Value a) 

type Env a = [(Var, Value a)] 
type MuEnv a = [(MuVar, Value a -> Value a)] 

varScopeErr :: Var -> Value a 
varScopeErr v = error $ unwords ["Out of scope λ variable:", show v] 

appErr :: Value a 
appErr = error "Trying to apply a non-lambda" 

muVarScopeErr :: MuVar -> (Value a -> Value a) 
muVarScopeErr alpha = id 

app :: Value a -> Value a -> Value a 
app (LamV f) x = f x 
app (MuV f) x = MuV $ \y -> f x `app` y 
app _ _ = appErr 

eval :: Env a -> MuEnv a -> Expr -> Value a 
eval env menv (Var v) = fromMaybe (varScopeErr v) $ lookup v env 
eval env menv (Lam v e) = LamV $ \x -> eval ((v, x):env) menv e 
eval env menv (Mu alpha beta e) = MuV $ \u -> 
    let menv' = (alpha, (`app` u)):menv 
     wrap = fromMaybe (muVarScopeErr beta) $ lookup beta menv' 
    in wrap (eval env menv' e) 
eval env menv (App f e) = eval env menv f `app` eval env menv e 

example 0 = App (App t (Var "v")) (Var "w") 
    where 
    t = Lam "x" $ Lam "y" $ Mu "delta" "phi" $ App (Var "x") (Var "y") 
example n = App (example (n-1)) (Var ("z_" ++ show n))