☰

PHOAS式の解析 質問する

tag-icon • tag-icon haskell
PHOAS式の解析 質問する

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

しかし、このような式のパーサーを構築する方法がわかりません。たとえば、"(lambda (a) a)"(対応する Haskell 値) を受け取って構築する方法lam $ \ x -> xです。(Text.Parsec または同様のものを使用する必要があります。)

de-Bruijn インデックスを使用してラムダ項を生成するパーサーを構築することはできますが、それは何の役に立つのでしょうか?

ベストアンサー1

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

デ・ブリュイン指数

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

おすすめ記事