Question

希腊字母约塔（ɩ）是可以添加到 SKI 演算里的另一个组合子。下面是它的规约规则：ɩ[α] 可以规约成 α[S][K]。

我们的 SKI 演算实现让加入一个新的组合子变得很容易：

IOTA = SKICombinator.new('ɩ')

# 规约ɩ [a] 为 a[S][K]
def IOTA.call(a)
  SKICall.new(SKICall.new(a, S), K)
end

def IOTA.callable?(*arguments)
  arguments.length == 1
end

Chris Barker 提 交了一种叫作Iota（http://semarch.linguistics.fas.nyu.edu/barker/Iota/） 的语 言，它的程序只使用 ɩ 组合子。尽管只有一个组合子，Iota 仍然是一种通用语言，因为任何 SKI 演算表达式都可以转成它，而我们已经看到 SKI 演算是通用的。

可以通过应用这些替换规则把 SKI 表达式转成 Iota：

· 用ɩ[ɩ[ɩ[ɩ[ɩ]]]] 替换 S；

· 用 ɩ[ɩ[ɩ[ɩ]]] 替换 K；

· 用 ɩ[ɩ] 替换 I。

很容易实现这个转换：

class SKISymbol
  def to_iota
    self
  end
end

class SKICall
  def to_iota
    SKICall.new(left.to_iota, right.to_iota)
  end
end

  def S.to_iota
    SKICall.new(IOTA, SKICall.new(IOTA, SKICall.new(IOTA, SKICall.new(IOTA, IOTA))))
  end

  def K.to_iota
    SKICall.new(IOTA, SKICall.new(IOTA, SKICall.new(IOTA, IOTA)))
  end

  def I.to_iota
    SKICall.new(IOTA, IOTA)
  end

S、K和 I 组合子的 Iota 版与原始表达式是否等价一点都不明显，因此我们可以通过规约SKI 演算内部的每一个组合子并观察它们的行为来进行研究。下面是在我们把 S 转换成 Iota 然后对其进行规约的过程：

>> expression = S.to_iota
=> ɩ[ɩ[ɩ[ɩ[ɩ]]]]
>> while expression.reducible?
    puts expression
    expression = expression.reduce
  end; puts expression
ɩ[ɩ[ɩ[ɩ[ɩ]]]]
ɩ[ɩ[ɩ[ɩ[S][K]]]]
ɩ[ɩ[ɩ[S[S][K][K]]]]
ɩ[ɩ[ɩ[S[K][K[K]]]]]
ɩ[ɩ[S[K][K[K]][S][K]]]
ɩ[ɩ[K[S][K[K][S]][K]]]
ɩ[ɩ[K[S][K][K]]]
ɩ[ɩ[S[K]]]
ɩ[S[K][S][K]]
ɩ[K[K][S[K]]]
ɩ[K]
K[S][K]
S
=> nil

是的，ɩ[ɩ[ɩ[ɩ[ɩ]]]] 实际上与 S等价。这同样也适用于 K：

>> expression = K.to_iota
=> ɩ[ɩ[ɩ[ɩ]]]
>> while expression.reducible?
    puts expression
    expression = expression.reduce
  end; puts expression
ɩ[ɩ[ɩ[ɩ]]]
ɩ[ɩ[ɩ[S][K]]]
ɩ[ɩ[S[S][K][K]]]
ɩ[ɩ[S[K][K[K]]]]
ɩ[S[K][K[K]][S][K]]
ɩ[K[S][K[K][S]][K]]
ɩ[K[S][K][K]]
ɩ[S[K]]
S[K][S][K]
K[K][S[K]]
K
=> nil

但对于I 则不行。ɩ 规约规则只会产生含有 S和 K组合子的表达式，因此不可能以字面量 I结束：

>> expression = I.to_iota
=> ɩ[ɩ]
>> while expression.reducible?
    puts expression
    expression = expression.reduce
  end; puts expression
ɩ[ɩ]
ɩ[S][K]
S[S][K][K]
S[K][K[K]]
=> nil

因此 S[K][K[K]] 在语法上与 I 不等价，但它是 S 和 K组合子表达式与 I 表达式做同样事情的另一个例子：

>> identity = SKICall.new(SKICall.new(S, K), SKICall.new(K, K))
=> S[K][K[K]]
>> expression = SKICall.new(identity, x)
=> S[K][K[K]][x]
>> while expression.reducible?
    puts expression
    expression = expression.reduce
  end; puts expression
S[K][K[K]][x]
K[x][K[K][x]]
K[x][K]
x
=> nil

所以到 Iota 的转换虽然没有完全保留所有三个 SKI 组合子的语法，但确实保留了它们的个体行为。我们可以通过把熟悉的 lambda 演算表达式用它的 SKI 演算表示转成 Iota 来测试整体的效果，然后对其求值以检查它的行为：

>> two
=> -> p { -> x { p[p[x]] } }
>> two.to_ski
=> S[S[K[S]][S[K[K]][I]]][S[S[K[S]][S[K[K]][I]]][K[I]]]
>> two.to_ski.to_iota
=> ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[
ɩ[ɩ[ɩ]]]]][ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]
]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ]]]]][ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ]]]]
>> expression = SKICall.new(SKICall.new(two.to_ski.to_iota, inc), zero)
=> ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[
ɩ[ɩ[ɩ]]]]][ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]
]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ]]]]][ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ]]]][inc][zero]
>> expression = expression.reduce while expression.reducible?
=> nil
>> expression
=> inc[inc[zero]]

inc[inc[zero]]是 我们所期望的结果，因此 Iota 表 达式ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ]]]]][ɩ[ɩ]]]] [ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]]]][ɩ[ɩ[ɩ[ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ[ɩ[ɩ]]]]][ɩ[ɩ]]]][ɩ[ɩ[ɩ[ɩ]]][ɩ[ɩ]]]] 实际是一个对->p{->x{p[p[x]]}} 进行无变量、无函数并且只有一个组合子的有效转换。而因为我们可以对任何 lambda 演算表达式进行这种转换，所以 Iota 是另一种通用语言。