实施 SKI 转型答案

【问题标题】：Implementing SKI transformation实施 SKI 转型
【发布时间】：2021-12-30 15:27:40
【问题描述】：

我需要实现以下算法才能将 Lambda 演算转换为组合逻辑。

规则来自https://en.wikipedia.org/wiki/Combinatory_logic#Completeness_of_the_S-K_basis

T[x] => x

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

T[λx.E] => (K T[E]) (if x does not occur free in E)

T[λx.x] => I

T[λx.λy.E] => T[λx.T[λy.E]] (if x occurs free in E)

T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂]) (if x occurs free in E₁ or E₂)

这是我目前所拥有的：

data CLExpr  =  S | K | I | CLVar Int | CLApp CLExpr CLExpr 

data LamExpr  =  LamApp LamExpr LamExpr  |  LamAbs Int LamExpr  |  LamVar Int 

skiTransform :: LamExpr -> CLExpr

skiTransform (LamVar x) = CLVar x --Rule 1

skiTransform (LamAbs y (s)) 
           | (free y s == False) = K (skiTransform(s)) --Rule 3

skiTransform (LamAbs x (LamVar y)) 
           | x == y     = I --Rule 4

skiTransform (LamAbs x (LamAbs y (s))) 
           | (free x s) = skiTransform 
                            (LamAbs x (skiTransform (LamAbs y (s)))) --Rule 5

free :: Int -> LamExpr -> Bool
free x (LamVar y) = x == y
free x (LamAbs y e) | x == y = False
free x (LamAbs y e) | x /= y = free x e
free x (LamApp e f) = (free x e) || (free x f)

我遇到的问题是，在规则 5 中，如何“嵌套”我的转换函数，如顶部所示。内部转换创建类型 CLExpr，然后不能将其用作外部转换的输入。

我也不确定如何实现规则 2 和 6，这需要分隔两个相邻的表达式，但这还不是优先事项。

谢谢！

【问题讨论】：

让两个组合子表达式彼此相邻意味着将它们一起应用。您的数据类型中已经有这种情况为CLApp。所以你将(A B) 表示为CLApp A B，将(S A B) 表示为CLApp (CLApp S A) B)。

标签： haskell lambda-calculus combinators

【解决方案1】：

要处理这种嵌套，您可以将源语言扩展为源语言和目标语言的超集（或者换句话说，泛化 LamExpr 以包含常量）。

-- The "union" of LamExpr and CLExpr
data LamCLExpr = S' | K' | I' | LCLVar Int | LCLApp CLExpr CLExpr | LCLAbs Int LamCLExpr

然后你可以定义两种语言的注入

fromLam :: LamExpr -> LamCLExpr
fromCL :: CLExpr -> LamCLExpr

这允许您定义转换

skiTransform :: LamCLExpr -> CLExpr

特别是在嵌套情况下使用fromCL。

【讨论】：