时间戳

首页 > 解决方案 > 避免捕获的替换函数 - Lambda 演算

haskell - 避免捕获的替换函数 - Lambda 演算

问题描述

所以我得到了下面的替代函数，我试图用它来替换示例术语中的教堂数字 0 的 b：

\一个。\X。(\y.a) xb

*Main> 替换“b”（数字 0）示例

目前正在给我：

\C。\一个。(\b.c) a (\f.\x.x)

但是我期待答案是：

\C。\一个。( \a . c) 一个 (\f. \x. x)

你能告诉我我在这里做错了什么吗，是使用新鲜的吗？此处的替换函数似乎没有将此处的“a”视为新变量，因为它已被用作先前 x 的替代品？有没有办法解决这个问题？

substitute :: Var -> Term -> Term -> Term
substitute x n (Variable y)| y == x = n
                           | otherwise = (Variable y)
substitute x n (Lambda y m)| y == x = (Lambda y m)
                           | otherwise = (Lambda new_z m')
                                 where
                                  new_z = fresh([x] `merge` (used m) `merge`(used n))
                                  m' = substitute x n (substitute y (Variable new_z) m)
substitute x n (Apply m1 m2) = (Apply new_m1 new_m2)
                                 where new_m1 = substitute x n m1
                                       new_m2 = substitute x n m2

在哪里

used :: Term -> [Var]
used (Variable z) = [z]
used (Lambda z n) = merge [z](used n)
used (Apply n m) = merge (used n)(used m)

和

fresh :: [Var] -> Var
fresh st = head (filterVariables variables st)

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

filterVariables :: [Var] -> [Var] -> [Var]
filterVariables s t = filter (`notElem` t) s

和

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

标签： haskelllambda-calculus

解决方案

从 lambda 演算的角度来看，在 中b是自由的\a. \x. (\y. a) x b，所以代替0给b，\a. \x. (\y. a) x 0如果0=\f. \x. x那么它是

\a. \x. (\y. a) x (\f. \x. x)
===
\c. \x. (\y. c) x (\f. \x. x)
===
\c. \x. (\b. c) x (\f. \x. x)

你显然得到

\c. \a. (\b. c) a (\f. \x. x)

这是相同的 lambda 项，直到 alpha 转换（一致的捕获避免重命名变量）。

所以没有错误。

推荐阅读