在Haskell中解释Parigot的lambda-mu演算 [英] interpret Parigot's lambda-mu calculus in Haskell

问题描述

我们可以解释Haskell中的lambda演算：

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

data a = V a | F（值a - >值a）

interpret :: [（String，Value a）] - > Expr - >值a
解释env（Var x）=案例查找x env of
Nothing - >错误未定义变量
只是v - > v
interpret env（Lam xe）= F（\ v - > interpret（（x，v）：env）e）
解释env（App e1 e2）= case解释en b $ b V _ - >错误不是函数
F f - > f（解释env e2）

上述解释器如何扩展到 lambda-mu微积分？我的猜测是它应该使用continuations来解释这个演算中的附加结构。 （ Bernardi& Moortgat论文中的（15）和（16）是我期望的那种翻译。

Haskell可能是图灵完成的，但是怎么做？

提示： strong>关于此研究论文，请参阅第197页上的评论直观的mu粘合剂的含义。

解决方案

下面是从文件中使用@ user2407038的表示（正如你所看到的，当我说无意识的时候，我的确有意无意义）：

  { - ＃LANGUAGE DataKinds，KindSignatures， GADTs＃ - } 
 { - ＃LANGUAGE StandaloneDeriving＃ - } 
 
 import Control.Monad.Writer 
 import Control.Applicative 
 import Data.Monoid 
 
 data TermType =命名|未命名
 
类型Var =字符串
类型MuVar =字符串
 
数据Expr（n :: TermType）其中
 Var :: Var  - > Expr未命名
 Lam :: Var  - > Expr未命名 - > Expr未命名
 App :: Expr未命名 - > Expr未命名 - > Expr未命名
 Freeze :: MuVar  - > Expr未命名 - > Expr命名为
 Mu :: MuVar  - > Expr命名 - > Expr未命名的
派生实例Show（Expr n）
 
 substU :: Var  - > Expr未命名 - > Expr n  - > Expr n 
 substU x e = go 
 where 
 go :: Expr n  - > Expr n $ b $ go（Var y）= if y == x then e else Var y 
 go（Lam ye）= Lam y $ if y == x then e else go e 
 go （App fe）= 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 
去（Var x）= Var x 
去（Lam xe）= Lam x（去e）
去（App fe）= App（去f）（去e）
 go（冻结伽马e）=冻结（如果伽马==贝塔尔然后阿尔法其他伽马）（去e）
去（穆伽伽）=穆伽伽$如果伽玛==贝塔尔然后你别去你
 
 appN :: MuVar  - > Expr未命名 - > Expr n  - > Expr n 
 appN beta v = go 
 where 
 go :: Expr n  - > Expr n 
去（Var x）= Var x 
去（Lam xe）= Lam x（去e）
去（App fe）= App（去f）（去e）
 go（Freeze alpha w）=如果alpha == beta，则冻结alpha $然后应用程序（转到）v否则转到w 
转到（Mu alpha u）= Mu alpha $ if alpha / = beta then go u else u 
 
 reduceTo :: a  - > Writer任何一个
 reduceTo x = tell（Any True）>> return x 
 
 reduce0 :: Expr n  - > Writer Any（Expr n）
 reduce0（App（Lam xu）v）= reduceTo $ substU xvu 
 reduce0（App（Mu beta u）v）= reduceTo $ Mu beta $ appN beta vu 
 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 =< （应用程序< $> reduce1 f * reduce1 e）
 reduce1（Freeze alpha e）= reduce0 =< （冻结alpha $ reduce1e）
 reduce1（Mu alpha u）= reduce0 =<< （Mu alpha< $> reduce1 u）
 
 reduce :: Expr n  - > Expr n 
 reduce e = case 
（e'，Any changed） - > runWriter（reduce1 e）如果改变了，那么减少e'else e 
  

/ p>

 示例0 = App（App t（Varx））（Vary）
 where 
t = Lamx$ Lamy$ Mudelta$ Freezephi$ App（Varx）（Vary）
例子n = App（例子））（Var（z_++ show n））
  

我可以减少 example n 到预期的结果：

  * Main>减少（示例10）
 Mudelta（Freezephi（App（Varx）（Vary）））
  

我之前在作品中引用恐吓引语的原因是我对λμ微积分没有直觉，所以我不知道它应该做什么。

One can interpret the lambda calculus in 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)

How could the above interpreter be extended to the lambda-mu calculus? My guess is that it should use continuations for interpreting the additional constructs in this calculus. (15) and (16) from the Bernardi&Moortgat paper are the kind of translations I expect.

It is possible since Haskell is Turing-complete, but how?

Hint: See the comment on page 197 on this research paper for the intuitive meaning of the mu binder.

解决方案

Here's a mindless transliteration of the reduction rules from the paper, using @user2407038's representation (as you'll see, when I say mindless, I really do mean mindless):

{-# 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

It "works" for the example from the paper: with

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

I can reduce example n to the expected result:

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

The reason I put scare quotes around "works" above is that I have no intuition about the λμ calculus so I don't know what it should do.

这篇关于在Haskell中解释Parigot的lambda-mu演算的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！