标签: s-combinator

S组合器的模拟是否可以仅使用标准函数(不通过公式定义)并且不使用lambda(匿名函数)在Haskell中表示？我期待它的类型(a -> b -> c) -> (a -> b) -> a -> c.

例如,K组合器的模拟就是const.

实际上我试图\f x -> f x x用标准函数来表达函数,但是不能想到任何标准的非线性函数(这是一个多次使用它的参数的函数).

我开始学习lambda演算,我需要在Erlang中实现I,S,K组合器.当然,S,K,我代表:

S =λxyz.xz(yz)K =λxy.xI=λx.x

我在纸上理解I = SKK转换没有问题(如此处所示:为了证明SKK和II是beta等价的,lambda演算)但似乎在功能语言和高阶函数时我不理解它. ..

我设法做了我和K(让我们说在模块中test):

i(X) -> X.
k(X) -> fun(Y) -> X end.

我也知道如何运行K x(K x)(SKK x = K x(K x))

kxk(X) -> (k(X))(k(X)).

但我无法理解它编写S组合器.我试过了:

s(X) -> fun (Y) -> fun(Z) -> X,Z (Y,Z) end end.

但是,我仍然无法将SKK x转换为x

我尝试像这样运行它:

skkx(X) ->  s((k((k(X))))).

任何帮助将不胜感激,因为我完全迷失了.

假设有一些数据类型来表达lambda和组合术语:

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)

还有一个函数来获取lambda术语的自由变量列表:

fv ? Eq ? ? Lam ? ? [?]
fv (Var v) = [v] …

我是lambda演算的新手,并努力证明以下内容.

SKK和II是等效的.

哪里

S = lambda xyz.xz(yz)K = lambda xy.x I = lambda xx

我尝试通过打开它来测试减少SKK,但无处可去,它变得凌乱.不要认为SKK可以在不扩展S,K的情况下进一步减少.

我试图实现一个简单类型的lambda演算类型检查器.运行完整性测试时,我尝试输入(SKK),我的类型检查器抛出此错误:

TypeMismatch {firstType = t -> t, secondType = t -> t -> t}

违规术语显然是(SKK)

(\x:t -> t -> t.\y:t -> t.\z:t.x z (y z)) (\x:t.\y:t.x) (\\x:t.\y:t.x)

我认为问题源于缺乏多态性,因为当我输入检查这个haskell代码时它工作正常:

k x y = x
s x y z = x z (y z)
test = s k k -- type checks

但如果我专注于这种类型:

k :: () -> () -> ()
k x y = x
s :: (() -> () -> ()) -> (() -> ()) -> () -> ()
s x …