Функция замены, позволяющая избежать захвата - лямбда-исчисление

Question

Я пытаюсь написать функцию, которая выполняет подстановку без захвата в лямбда-исчислении. Код компилируется, но не выдает правильный ответ. Я написал то, что, как я ожидаю, должен делать код, правильное ли мое понимание?

Например, я должен получить следующий вывод для этого ввода (numeral 0 - это церковная цифра 0)

*Main> substitute "b" (numeral 0) example    -- \a. \x. ((\y. a) x) b
\c. \a. (\a. c) a (\f. \x. x)

-- The incorrect result I actually got
\c. \c. (\f. \x. x) (x (\b. a))

NB \y переименовано в \a из-за замены (\y.a)[N/b] (я думаю, что это описано в коде, который я написал, но, пожалуйста, дайте мне знать, если я ошибаюсь .)

import Data.Char
import Data.List

type Var = String

data Term =
    Variable Var
  | Lambda   Var  Term
  | Apply    Term Term
  --  deriving Show

instance Show Term where
  show = pretty

example :: Term        -- \a. \x. ((\y. a) x) b
example = Lambda "a"
            (Lambda "x" (Apply (Apply (Lambda "y" (Variable "a")) 
                                      (Variable "x")) 
                               (Variable "b")))

pretty :: Term -> String
pretty = f 0
    where
      f i (Variable x) = x
      f i (Lambda x m) = if i /= 0 then "(" ++ s ++ ")" else s 
                         where s = "\\" ++ x ++ ". " ++ f 0 m 
      f i (Apply  n m) = if i == 2 then "(" ++ s ++ ")" else s 
                         where s = f 1 n ++ " " ++ f 2 m

substitute :: Var -> Term -> Term -> Term

substitute x n (Variable y)  
    --if y = x, then leave n alone   
    | y == x    = n
    -- otherwise change to y  
    | otherwise = Variable y

substitute x n (Lambda y m)
    --(\y.M)[N/x] = \y.M if y = x 
    | y == x    = Lambda y m
    --otherwise \z.(M[z/y][N/x]), where `z` is a fresh variable name 
    --generated by the `fresh` function, `z` must not be used in M or N, 
    --and `z` cannot be equal `x`. The `used` function checks if a 
    --variable name has been used in `Lambda y m`   
    | otherwise = Lambda newZ newM
                  where newZ = fresh(used(Lambda y m))
                        newM = substitute x n m          

substitute x n (Apply  m2 m1) = Apply newM2 newM1
    where newM1 = substitute x n m2
          newM2 = substitute x n m1

used :: Term -> [Var]
used (Variable n) = [n]
used (Lambda n t) = merge [n] (used t)
used (Apply t1 t2) = merge (used t1) (used t2)

variables :: [Var]
variables =  [l:[] | l <- ['a'..'z']] ++ 
             [l:show x | x <- [1..], l <- ['a'..'z']]

filterFreshVariables :: [Var] -> [Var] -> [Var]
filterFreshVariables lst = filter ( `notElem` lst)

fresh :: [Var] -> Var
fresh lst = head (filterFreshVariables lst variables)

recursiveNumeral :: Int -> Term
recursiveNumeral i
  | i == 0 = Variable "x"
  | i > 0 = Apply(Variable "f")(recursiveNumeral(i-1))

numeral :: Int -> Term
numeral i = Lambda "f" (Lambda "x" (recursiveNumeral i))

merge :: Ord a => [a] -> [a] -> [a]
merge (x : xs) (y : ys)
  | x < y = x : merge xs (y : ys)
  | otherwise = y : merge (x : xs) ys
merge xs [] = xs
merge [] ys = ys

Answer 1

Эта часть в substitute x n (Lambda y m) неверна:

• комментарий гласит: "z нельзя использовать в M или N", но ничто не мешает этому. newZ может быть переменной в n, что приводит к проблемному c захвату
• замена z/y не была выполнена

    | otherwise = Lambda newZ newM
                  where newZ = fresh(used(Lambda y m))
                        newM = substitute x n m

Исправлено:

1. "z нельзя использовать в M или N":

newZ = fresh(used m `merge` used n)

"M[z/y][N/x]":

newM = substitute x n (substitute y (Variable newZ) m)

Соедините:

    | otherwise = Lambda newZ newM
    where
      newZ = fresh(used m `merge` used n)
      newM = substitute x n (substitute y (Variable newZ) m)

Обратите внимание, что обновление всех привязок, как сделано выше, затрудняет понять результат и отладить подстановку. На самом деле y нужно обновлять только если y в n. В противном случае вы можете оставить y, добавив следующее предложение:

    | y `notElem` used n = Lambda y (substitute x n m)

Другая идея заключается в изменении fresh для выбора имени, похожего на старое, например, добавляя цифры до тех пор, пока не произойдет cla sh.

---

Все еще есть ошибка, которую я пропустил: newZ также не должен быть равен x (переменная, изначально подставляемая).

-- substitute [a -> \f. \x. x] in (\g. g), should be (\g. g)
ghci> substitute "a" (numeral 0) (Lambda "g" (Variable "g"))
\a. \g. \x. x

Два способа решения этой проблемы:

1. добавить x к набору переменных для исключения newZ из:

   newZ = fresh ([x] `merge` used m `merge` used n)
   

2. если вы подумаете об этом, эта ошибка проявляется только тогда, когда x отсутствует в m, и в этом случае заменить нечего, поэтому можно добавить еще одну ветку, пропускающую работу:

   | x `notElem` used m = Lambda y m
   

---

Составить:

substitute x n (Lambda y m)
    --(\y.M)[N/x] = \y.M if y = x 
    | y == x    = Lambda y m
    | x `notElem` used m = Lambda y m
    | y `notElem` used n = Lambda y (substitute x n m)
    | otherwise = Lambda newZ newM
                  where newZ = fresh(used m `merge` used n)
                        newM = substitute x n (substitute y (Variable newZ) m)

Вывод

ghci> example
\a. \x. (\y. a) x b
ghci> numeral 0
\f. \x. x
ghci> substitute "b" (numeral 0) example
\a. \c. (\y. a) c (\f. \x. x)

---

Примечание. Я не пытался доказать этот код правильно ( упражнение для читателя: определите «правильно»), могут еще быть ошибки, которые я пропустил. Должен быть какой-то курс о лямбда-исчислении, в котором есть все детали и подводные камни, но я не потрудился посмотреть.