20

私は PHOAS (パラメトリック高次抽象構文) を理解していると思います。また、式をきれいに印刷する方法も理解しています ( http://www.reddit.com/r/haskell/comments/1mo59h/phoas_for_free_by_edward_kmett/ccbxzooを参照) 。 .

"(lambda (a) a)"しかし、そのような式のパーサーを構築する方法がわかりませんlam $ \ x -> x。(そして、Text.Parsec などを使用する必要があります。)

de-Bruijn 索引付けを使用してラムダ項を生成するパーサーを作成できますが、それは何に役立ちますか?

4

3 に答える 3

22

jozefg が言うように、操作間で簡単に変換できます。名前付き、de-Bruijn、およびラムダ項の PHOAS 表現の間で変換する方法を示します。絶対に必要な場合は、それをパーサーに融合するのは比較的簡単ですが、最初に名前付き表現を解析してから変換する方がおそらく良いでしょう。

仮定しましょう

import Data.Map (Map)
import qualified Data.Map as M

ラムダ項の次の 3 つの表現:

Stringに基づく名前

data LamN = VarN Name | AppN LamN LamN | AbsN Name LamN
  deriving (Eq, Show)

type Name = String

de-Bruijn 指数

data LamB = VarB Int | AppB LamB LamB | AbsB LamB
  deriving (Eq, Show)

フォーアス

data LamP a = VarP a | AppP (LamP a) (LamP a) | AbsP (a -> LamP a)

ここで、LamP とその他の間の変換 (両方向) を行います。これらは部分的な関数であることに注意してください。自由変数を含むラムダ項にそれらを適用する場合は、適切な環境を渡す責任があります。

からLamNへの行き方LamP

環境マッピング名を PHOAS 変数に取ります。クローズド タームでは、環境を空にすることができます。

lamNtoP :: LamN -> Map Name a -> LamP a
lamNtoP (VarN n)     env = VarP (env M.! n)
lamNtoP (AppN e1 e2) env = AppP (lamNtoP e1 env) (lamNtoP e2 env)
lamNtoP (AbsN n e)   env = AbsP (\ x -> lamNtoP e (M.insert n x env))

からLamBへの行き方LamP

PHOAS 変数のリストである環境を受け取ります。閉じた用語の空のリストにすることができます。

lamBtoP :: LamB -> [a] -> LamP a
lamBtoP (VarB n)     env = VarP (env !! n)
lamBtoP (AppB e1 e2) env = AppP (lamBtoP e1 env) (lamBtoP e2 env)
lamBtoP (AbsB e)     env = AbsP (\ x -> lamBtoP e (x : env))

「LamP」から「LamN」への移動方法

潜在的な自由変数をその名前にインスタンス化する必要があります。バインダーの名前を生成するための名前の供給を受け取ります。相互に異なる名前の無限リストにインスタンス化する必要があります。

lamPtoN :: LamP Name -> [Name] -> LamN
lamPtoN (VarP n)         _sup  = VarN n
lamPtoN (AppP e1 e2)      sup  = AppN (lamPtoN e1 sup) (lamPtoN e2 sup)
lamPtoN (AbsP f)     (n : sup) = AbsN n (lamPtoN (f n) sup)

「LamP」から「LamB」への取得方法

潜在的な自由変数を数値にインスタンス化する必要があります。現在使用しているバインダーの数を示すオフセットを取得します。0クローズドターム用にインスタンス化する必要があります。

lamPtoB :: LamP Int -> Int -> LamB
lamPtoB (VarP n)     off = VarB (off - n)
lamPtoB (AppP e1 e2) off = AppB (lamPtoB e1 off) (lamPtoB e2 off)
lamPtoB (AbsP f)     off = AbsB (lamPtoB (f (off + 1)) (off + 1))

例

-- \ x y -> x (\ z -> z x y) y

sample :: LamN
sample = AbsN "x" (AbsN "y"
  (VarN "x" `AppN` (AbsN "z" (VarN "z" `AppN` VarN "x" `AppN` VarN "y"))
            `AppN` (VarN "y")))

PHOAS 経由で de-Bruijn に移動:

ghci> lamPtoB (lamNtoP sample M.empty) 0
AbsB (AbsB (AppB (AppB (VarB 1) (AbsB (AppB (AppB (VarB 0) (VarB 2)) (VarB 1)))) (VarB 0)))

PHOAS 経由で名前に戻る:

ghci> lamPtoN (lamNtoP sample M.empty) [ "x" ++ show n | n <- [1..] ]
AbsN "x1" (AbsN "x2" (AppN (AppN (VarN "x1") (AbsN "x3" (AppN (AppN (VarN "x3") (VarN "x1")) (VarN "x2")))) (VarN "x2")))
于 2013-10-17T07:09:13.577 に答える
6

jozefg のコメントには正しい答えがあります。巧妙な表現ではなく、常に単純な抽象構文ツリーに解析します。次に、解析後、表現を変換します。この場合は簡単

data Named = NLam String Named | NVar String | NApp Named Named

convert :: (String -> a) -> Named -> Exp a a
convert f (NVar n) = var $ f n
convert f (NApp e1 e2) = app (convert f e1) (convert f e2)
convert f (NLam s e) = lam $ \a -> convert (nf a) e where
  nf a s' = if s' == s then a else f s'

もちろん、マップとして関数以外のものを使用することもできString -> aます。 Data.Mapたとえば、線形時間ルックアップを取り除きます。

他の HOAS スキームよりも PHOAS が優れている点の 1 つは、簡単に「元に戻す」ことができることです。

addNames :: ExpF Int (State Int Named) -> State Int Named
addNames (App a b) = liftM2 NApp a b
addNames (Lam f)   = do
  i <- get
  put (i + 1)
  r <- f i
  return $ NLam ('x':show i) r

convert' :: Exp Int Int -> Named
convert' = fst 
  . flip runState 0
  . cata addNames 
  . liftM (return . NVar . ('x':) . show)

期待どおりに動作します

λ: convert' $ convert undefined $ NLam "x" $ NApp (NVar "x") (NLam "y" (NVar "y"))
> NLam "x0" (NApp (NVar "x0") (NLam "x1" (NVar "x1")))
于 2013-10-17T06:30:55.477 に答える
3

ここで他の回答のテーマで再度実行し、名前付き変数を使用して単純な表現を作成しているだけであるかのように解析することをお勧めします。中間表現を避けたい場合は、理解を難しくすることなく、パーサーにインライン化できます。

data Lam a = Var a | Lam a `App` Lam a | Lam (a -> Lam a)

type MkLam a = (String -> a) -> Lam a

var :: String -> MkLam a
var x = Var . ($ x)

app :: MkLam a -> MkLam a -> MkLam a
app = liftA2 App

lam :: String -> MkLam a -> MkLam a
lam v e env = Lam $ \x -> e $ \v' -> if v == v' then x else env v'

パーサーで中間表現のコンストラクターを使用する代わりに、これらの関数を直接使用するという考え方です。それらはコンストラクターと同じ型を持っているため、実際には単なるドロップイン置換です。また、ADT とインタープリターを個別に記述する必要がないため、少し短くなります。

于 2013-10-23T04:00:31.920 に答える