4

我正在用组合逻辑进行一些定理证明实验，这看起来很有希望，但有一个绊脚石：有人指出，在组合逻辑中，例如 I = SKK 是真的，但这不是一个定理，它必须作为公理添加。有谁知道需要添加的公理的完整列表？

编辑：您当然可以手动证明 I = SKK，但除非我遗漏了什么，否则它不是具有相等性的组合逻辑系统中的定理。话虽如此，您可以将 I 宏扩展为 SKK ......但我仍然缺少一些重要的东西。取一组子句 p(X) 和 ~p(X)，它们很容易解决普通一阶逻辑中的矛盾，并将它们转换为 SK，执行替换并评估 S 和 K 的所有调用，我的程序生成以下（我使用 ' 作为 Unlambda 的反引号）：

''eq '''s ''s 'ks ''s 'ks '' kk 'k eq ''s 'ks 'kk 'kk ''s 'kk 'k 假'k 真的'k 真的

看起来我可能需要一套适当的规则来处理部分调用'k和''，我只是没有看到这些规则应该是什么，我在这个领域能找到的所有文献都是为目标受众是数学家而不是程序员。我怀疑一旦你理解了答案，答案可能很简单。

4

3 回答 3

8

一些教科书将I定义为((SK) K)的别名。在这种情况下，根据定义它们它们是相同的（作为术语）。为了证明它们的相等性（作为函数），我们只需要证明相等性是自反的，这可以通过自反公理方案来实现：

  • 命题 `` E = E '' 是可推导的（反身公理方案，为此处由元变量E表示的每个可能项实例化）

因此，我想在下文中，您的问题调查了另一种方法：当组合子I未被定义为复合术语((SK) K)的别名时，而是作为独立的基本组合子常量单独引入时，其操作语义由公理方案显式声明

  • ``( I E ) = E '' 是可推导的（I-公理方案）

我想你的问题问

我们是否可以正式推断（保留在系统内部） ，当用作归约中的函数时，这种独立定义的I的行为与((SK) K)完全相同 ？

我认为我们可以，但我们必须求助于更强大的工具。我猜想通常的公理方案是不够的，我们还必须声明可扩展性属性（函数相等），这是重点。如果我们想将外延性形式化为一个公理，我们必须用自由变量来扩充我们的对象语言。

我认为，我们必须采用这种方法来构建组合逻辑，即我们还必须允许在对象语言中使用变量。当然，我的意思是“只是”免费的贵重物品。使用绑定变量会作弊，我们必须保持在组合逻辑的范围内。使用免费变量不是作弊，它是一个诚实的工具。因此，我们可以做您需要的正式证明。

除了直接的等式公理和推理规则（及物性、自反性、对称性、莱布尼茨规则）外，我们还必须为等式添加一个推理的外延规则。这是自由变量很重要的一点。

在 Csörnyei 2007: 157-158 中，我发现了以下方法。我认为这样可以完成证明。

一些备注：

大多数公理实际上是公理方案，由无限多个公理实例组成。必须为每个可能的E、F、G项实例化实例。在这里，我使用斜体表示元变量。

公理方案的表面无限本质不会引发可计算性问题，因为它们可以在有限时间内解决：我们的公理系统是递归的。这意味着一个聪明的解析器可以在有限的时间内（而且非常有效地）决定一个给定的命题是否是一个公理方案的一个实例。因此，公理方案的使用既不会引起理论问题，也不会产生实际问题。

现在让我们看看我们的框架：

语言

字母

常量：以下三个称为常量：K、S、I。

我添加了常量I只是因为您的问题假定我们没有将组合子I定义为复合术语S K K的别名/宏，但它本身就是一个独立的常量。

我将用粗体大写字母表示常数。

应用程序符号：“应用程序”的符号 @ 就足够了（带有 arity 2 的前缀符号）。作为语法糖，我在这里使用括号而不是显式的应用程序符号：我将使用显式的打开（和关闭）符号。

变量：虽然组合逻辑不使用绑定变量、范围等，但我们可以引入自由变量。我怀疑，它们不仅是句法糖，还可以加强演绎系统。我猜想，您的问题将需要使用它们。任何可枚举的无限集（不相交的常数和括号符号）都将用作变量的字母表，我将在这里用未格式化的罗马小写字母 x、y、z 来表示它们...

条款

术语是归纳定义的：

  • 任何常数都是一个术语
  • 任何变量都是一个术语
  • 如果E是一个项，而F也是一个项，那么 ( E F ) 也是一个项

我有时使用实用的约定作为语法糖，例如写

E F G H

代替

（（（E F）G）H）。

扣除

转换公理方案：

  • `` K E F = E '' 是可推导的（K-公理方案）
  • `` S F G H = F H ( G H )'' 是可推导的（S-公理方案）
  • `` I E = E '' 是可推导的（I-公理方案）

我添加第三个转换公理（I规则）只是因为您的问题预设了我们没有将组合子I定义为S K K的别名/宏。

等式公理方案和推理规则

  • `` E = E '' 是可推导的（反身公理）
  • 如果“ E = F ”是可演绎的，那么“ F = E ”也是可演绎的（推理的对称规则）
  • 如果“ E = F ”是可演绎的，并且“ F = G ”也是可演绎的，那么“ E = G ”也是可约的（传递性规则）
  • 如果“ E = F ”是可演绎的，那么“ E G = F G ”也是可演绎的（莱布尼茨规则I）
  • 如果“ E = F ”是可演绎的，那么“ G E = G F ”也是可演绎的（莱布尼茨规则II）

问题

现在让我们调查你的问题。我猜想到目前为止定义的演绎系统不足以证明你的问题。

命题“ I = S K K ”是否可演绎？

问题是，我们必须证明函数的等价性。如果两个函数的行为方式相同，我们就认为它们是等效的。函数的作用是将它们应用于参数。如果应用于每个可能的参数，我们应该证明两个函数的行为方式相同。再次，无穷大的问题！我怀疑，公理方案在这里无法帮助我们。就像是

如果E F = G F是可演绎的，那么E = G也是可演绎的

将无法完成这项工作：我们可以看到这不会产生我们想要的。使用它，我们可以证明

`` I E = S K K E '' 是可演绎的

对于每个E项实例，但这些结果只是单独的实例，不能作为一个整体进一步推演。我们只有具体的结果（无限多），无法总结：

  • 它适用于E := K
  • 为E := S成立
  • 它适用于E := K K
  • .
  • .
  • .

...

我们不能将这些零散的结果实例总结为一个伟大的结果，说明可扩展性！我们不能将这些低价值的片段倒入漏斗中，以推理规则将它们融合成一个更有价值的结果。

我们必须增强我们的演绎系统的力量。我们必须找到一个可以抓住问题的正式工具。你的问题导致了外延性，我认为，声明外延性需要我们可以提出适用于 ***** 任意 ***** 实例的命题。这就是为什么我认为我们必须在我们的对象语言中允许自由变量。我猜想以下额外的推理规则会起作用：

  • 如果变量 x 既不是E也不是F项的一部分，并且语句 ( E x) = ( F x) 是可演绎的，那么E = F也是可演绎的（推理的可扩展性规则）

这个公理的难点，容易导致混淆：x是对象变量，是我们对象语言的完全解放和尊重的部分，而E和G是元变量，不是对象语言的一部分，只是用于简洁的表示法的公理方案。

（备注：更准确地说，推理的外延规则应该以更谨慎的方式形式化，在所有可能的对象变量 x、y、z... 上引入元变量x ，以及在所有可能的对象变量上引入另一种元变量E术语实例。但是这两种元变量加上对象变量之间的区别在这里并不是那么具有指导意义，它不会对您的问题产生太大影响。）

证明

现在让我们证明“ I = S K K ”这个命题。

左侧步骤：

  • 命题 `` I x = x'' 是具有实例化[ E := x]的I-公理方案的一个实例

右手边的步骤：

  • 命题“ S K K x = K x ( K x)”是具有实例化[ E := K , F := K , G := x]的S-公理方案的一个实例，因此它是可推导出的
  • 命题“ K x ( K x) = x”是具有实例化[ E := x, F := K x]的K-公理方案的一个实例，因此它是可推导出的

等式的传递性：

  • 陈述“ S K K x = K x ( K x)”符合传递性推理规则的第一个前提，而陈述“ K x ( K x) = x”符合该推理规则的第二个前提。实例化为 [ E := S K K x, F := K x ( K x), G = x]。因此结论也成立：E = G。用相同的实例重写结论，我们得到语句“ S K Kx = x"，因此，这是可推导出的。

相等的对称性：

  • 使用“ S K K x = x”，我们可以推断出“x = S K K x”

等式的传递性：

  • 使用“ I x = x”和“x = S K K x”，我们可以推断出“ I x = S K K x”

现在我们已经为关键点铺平了道路：

  • 命题“ I x = S K K x”符合推理扩展规则的第一个前提：( E x) = ( F x)，具有实例化[ E := I , F := S K K ]。因此结论也必须成立，即“ E = F ”具有相同的实例化（[ E := I , F := S K K ]），产生命题“ I = S K K", quod erat demostrandum。

Csörnyei, Zoltán (2007)：Lambda-kalkulus。一个 funkcionális programozás alapjai。布达佩斯：Typotex。ISBN-978-963-9664-46-3。

于 2009-09-08T15:43:57.387 回答
3

您不需要将 I 定义为公理。从以下内容开始：

I.x = x
K.x y = x
S.x y z = x z (y z)

因为, then是一个恒等函数，就像.SKanything = anythingSKanythingI

所以，I = SKK和I = SKS。无需将 I 定义为公理，您可以将其定义为别名 SKK 的语法糖。

S 和 K 的定义只是公理。

于 2009-09-03T17:54:37.150 回答
0

对于 beta 相等，通常的公理是完整的，但不给出 eta 相等。Curry 发现了一组大约 30 个公理来获得 beta-eta 等式的完整性。它们列在 Hindley & Seldin 的组合器和 lambda 演算简介中。

Curry 的最后一个问题Roger Hindley列出了我们可能希望从 lambda 演算之间的映射中获得的一些额外需求，并指出我们没有满足所有这些需求的映射。您可能不会太在意所有标准。

于 2010-02-01T13:31:54.377 回答