Преобразование лямбда-термина в комбинаторный термин
Предположим, есть несколько типов данных для выражения лямбда и комбинаторных терминов:
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]) (если x не существует свободно в E)
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 ответа
Рассмотрим уравнение T[λx.λy.E] => T[λx.T[λy.E]].
Мы знаем, что результат T [λy.E] является выражением SKI. Так как это было произведено одним из случаев 3, 4 или 6, это либо я, либо приложение (:@).
Таким образом, внешний T в T [λx.T [λy.E]] должен быть одним из случаев 3 или 6. Вы можете выполнить этот анализ случая в коде. Извините, но у меня нет времени, чтобы написать это.
Ключевым моментом является то, что S, K и I - просто постоянные члены Лама, так же как 1, 2 и 3 - постоянные числа. Было бы довольно легко выполнить проверку типа по правилу 5, сделав обратную функцию 'convert':
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 y e))" справа. Поскольку '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'.
Вы, наверное, заметили, что я на самом деле назвал этот конструктор "Com", потому что это просто свернутый COMbinator, но я подумал, что было бы более информативно взять немного более длинный маршрут, чем просто сказать "заверните свои SKI в Lams":)
Если вам интересно, почему я назвал эту функцию "nvert", см. http://unapologetic.wordpress.com/2007/05/31/duality-terminology/:)
Варбо прав, комбинаторы - это постоянные лямбда-члены, следовательно, функция преобразованияT[ ]:L -> C с L множество лямбда-термов, а C - комбинаторных слагаемых и с C ⊂ L .
Таким образом, нет никаких проблем с печатанием для правила T[λx.λy.E] => T[λx.T[λy.E]]
Вот реализация в Scala.
Здесь лучше иметь общий тип данных для комбинаторов и лямбда-выражений. Обратите внимание, что ваши типы уже имеют значительное перекрытие (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