6

ラムダと組み合わせ項を表すデータ型がいくつかあるとします。

data Lam α = Var α                   -- v
           | Abs α (Lam α)           -- λv . e1
           | App (Lam α) (Lam α)     -- e1 e2
             deriving (Eq, Show)

infixl 0 :@
data SKI α = V α                     -- x
           | SKI α :@ SKI α          -- e1 e2
           | I                       -- I
           | K                       -- K
           | S                       -- S
             deriving (Eq, Show)

ラムダ項の自由変数のリストを取得する関数もあります。

fv ∷ Eq α ⇒ Lam α → [α]
fv (Var v) = [v]
fv (Abs x e) = filter (/= x) $ fv e
fv (App e1 e2) = fv e1 ++ fv e2

ラムダ項を組み合わせ項に変換するには、抽象的な排除規則が役立ちます。

convert ∷ Eq α ⇒ Lam α → SKI α

1) T[x] => x

convert (Var x) = V x

2) T[(E₁ E₂)] => (T[E₁] T[E₂])

convert (App e1 e2) = (convert e1) :@ (convert e2)

3) T[λx.E] => (KT[E]) (E で x が自由に発生しない場合)

convert (Abs x e) | x `notElem` fv e = K :@ (convert e)

4) T[λx.x] => I

convert (Abs x (Var y)) = if x == y then I else K :@ V y

5) T[λx.λy.E] => T[λx.T[λy.E]] (x が E に自由に現れる場合)

convert (Abs x (Abs y e)) | x `elem` fv e = convert (Abs x (convert (Abs y e)))

6) T[λx.(E₁ E₂)] => (ST[λx.E₁] T[λx.E₂])

convert (Abs x (App y z)) = S :@ (convert (Abs x y)) :@ (convert (Abs x z))

convert  _ = error ":["

この定義は次の理由で有効ではありません5):

Couldn't match expected type `Lam α' with actual type `SKI α'
In the return type of a call of `convert'
In the second argument of `Abs', namely `(convert (Abs y e))'
In the first argument of `convert', namely
  `(Abs x (convert (Abs y e)))'

だから、私が今持っているものは次のとおりです。

> convert $ Abs "x" $ Abs "y" $ App (Var "y") (Var "x")
*** Exception: :[

私が欲しいのは（私がそれを正しく計算することを願っています）：

> convert $ Abs "x" $ Abs "y" $ App (Var "y") (Var "x")
S :@ (S (KS) (S (KK) I)) (S (KK) I)

質問:

ラムダ項と組み合わせ項が異なるタイプの表現を持っている場合、どの5)ように定式化できますか?

4

4 に答える 4

1

ここでは、コンビネータとラムダ式に共通のデータ型を使用することをお勧めします。型にはすでにかなりのオーバーラップ（Var、App）があり、ラムダ式にコンビネータが含まれていても問題はありません。

排除したい唯一の可能性は、コンビネータ用語でラムダ抽象化を行うことです。インデックス付きの型を使用してそれらを禁止することができます。

次のコードでは、用語のタイプは、その用語にネストされたラムダ抽象化の数によってパラメーター化されます。convert関数は、を返します。Term Z aここで、Zはゼロを意味するため、返される項にラムダ抽象化はありません。

シングルトン型（ここで少し使用されています）の詳細については、論文「シングルトンを使用した依存型プログラミング」を参照してください。

{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, GADTs, TypeOperators,
    ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances #-}

data Nat = Z | Inc Nat

data SNat :: Nat -> * where
  SZ :: SNat Z
  SInc :: NatSingleton n => SNat n -> SNat (Inc n)

class NatSingleton (a :: Nat) where
  sing :: SNat a

instance NatSingleton Z where sing = SZ
instance NatSingleton a => NatSingleton (Inc a) where sing = SInc sing

type family Max (a :: Nat) (b :: Nat) :: Nat
type instance Max Z a = a
type instance Max a Z = a
type instance Max (Inc a) (Inc b) = Inc (Max a b)

data Term (l :: Nat) a where
  Var :: a -> Term Z a
  Abs :: NatSingleton l => a -> Term l a -> Term (Inc l) a
  App :: (NatSingleton l1, NatSingleton l2)
      => Term l1 a -> Term l2 a -> Term (Max l1 l2) a
  I   :: Term Z a
  K   :: Term Z a
  S   :: Term Z a

fv :: Eq a => Term l a -> [a]
fv (Var v) = [v]
fv (Abs x e) = filter (/= x) $ fv e
fv (App e1 e2) = fv e1 ++ fv e2
fv _ = []

eliminateLambda :: (Eq a, NatSingleton l) => Term (Inc l) a -> Term l a
eliminateLambda t =
  case t of
    Abs x t ->
      case t of
        Var y
          | y == x -> I
          | otherwise -> App K (Var y)
        Abs {} -> Abs x $ eliminateLambda t
        App a b -> S `App` (eliminateLambda $ Abs x a)
                     `App` (eliminateLambda $ Abs x b)
    App a b -> eliminateLambdaApp a b

eliminateLambdaApp
  :: forall a l1 l2 l . 
     (Eq a, Max l1 l2 ~ Inc l,
      NatSingleton l1,
      NatSingleton l2)
  => Term l1 a -> Term l2 a -> Term l a
eliminateLambdaApp a b =
  case (sing :: SNat l1, sing :: SNat l2) of
    (SInc _, SZ    ) -> App (eliminateLambda a) b
    (SZ    , SInc _) -> App a (eliminateLambda b)
    (SInc _, SInc _) -> App (eliminateLambda a) (eliminateLambda b)

convert :: forall a l . Eq a => NatSingleton l => Term l a -> Term Z a
convert t =
  case sing :: SNat l of
    SZ -> t
    SInc _ -> convert $ eliminateLambda t
于 2012-10-22T08:35:27.977 に答える
1

重要な洞察は、1、2、および 3 が定数 Int であるのと同じように、S、K、および I が単なる定数 Lam 項であるということです。「convert」関数を逆にすることで、ルール 5 の型チェックを行うのは非常に簡単です。

nvert :: SKI a -> Lam a
nvert S = Abs "x" (Abs "y" (Abs "z" (App (App (Var "x") (Var "z")) (App (Var "y") (Var "z")))))
nvert K = Abs "x" (Abs "y" (Var "x"))
nvert I = Abs "x" (Var "x")
nvert (V x) = Var x
nvert (x :@ y) = App (nvert x) (nvert y)

これで、「nvert」を使用してルール 5 の型チェックを行うことができます。

convert (Abs x (Abs y e)) | x `elem` fv e = convert (Abs x (nvert (convert (Abs y e))))

左側の「Abs y e」が右側の「nvert (convert (Abs ye))」に置き換えられていることを除いて、左と右が同じであることがわかります (ガードは無視します)。'convert' と 'nvert' は互いに逆であるため、任意の Lam 'x' を 'nvert (convert x)' にいつでも置き換えることができ、同様に、任意の SKI 'x' をいつでも 'convert (nvert x)' に置き換えることができます。 、したがって、これは有効な方程式です。

残念ながら、これは有効な方程式ですが、計算が進行しないため、有用な関数定義ではありません。「Abs y e」を永遠に前後に変換するだけです!

このループを断ち切るために、「nvert」への呼び出しを、後で実行する必要がある「リマインダー」に置き換えることができます。これを行うには、Lam に新しいコンストラクターを追加します。

data Lam a = Var a                   -- v
           | Abs a (Lam a)           -- \v . e1
           | App (Lam a) (Lam a)     -- e1 e2
           | Com (SKI a)             -- Reminder to COMe back later and nvert
             deriving (Eq, Show)

ルール 5 では、「nvert」の代わりに次のリマインダーを使用します。

convert (Abs x (Abs y e)) | x `elem` fv e = convert (Abs x (Com (convert (Abs y e))))

次のように、リマインダーを「nvert」の実際の呼び出しに置き換える別のルールを作成することで、戻ってくるという約束を果たす必要があります。

convert (Com c) = convert (nvert c)

これで、ようやくループを破ることができます。'convert (nvert c)' は常に 'c' と同じであることがわかっているため、上記の行を次のように置き換えることができます。

convert (Com c) = c

「convert」の最終的な定義では、実際には「nvert」をまったく使用していないことに注意してください。ただし、Lam を含む他の関数が新しい 'Com' ケースを処理するために使用できるため、これはまだ便利な関数です。

このコンストラクターは単なるラップアップ COMbinator であるため、実際に「Com」という名前を付けたことにお気付きかもしれませんが、単に「SKI を Lams でラップする」と言うよりも、少し長いルートを使用した方が有益であると考えました。 :)

なぜ私がその関数を「nvert」と呼んだのか疑問に思っている場合は、http://unapologetic.wordpress.com/2007/05/31/duality-terminology/ を参照してください:)

于 2014-01-24T17:09:16.130 に答える
1

方程式 T[λx.λy.E] => T[λx.T[λy.E]] を考えてみましょう。

T[λy.E] の結果は SKI 式であることがわかっています。ケース３、４、６のいずれかで作成されているので、Ｉかアプリケーション（:@）のいずれかです。

したがって、T[λx.T[λy.E]] の外側の T はケース 3 または 6 のいずれかでなければなりません。コードでこのケース分析を実行できます。申し訳ありませんが、それを書き出す時間がありません。

于 2012-10-21T21:18:22.620 に答える