functional-programming - 使用高阶逻辑定义“对”的概念

Question

修改自动推理课程，我不太明白如何回答这个问题：

展示如何(x, y)使用 lambda 抽象在高阶逻辑中定义对的概念。定义一个函数 π1，它返回这种对的第一个元素。最后，证明π1(x, y) = x.

我在 stackoverflow 上发现了类似的问题，但它们都与我从未使用过的方案有关。英文/相关数学符号的解释将不胜感激

Answer 1

干得好

PAIR := λx. λy. λp. p x y

π1 := λp. p (λx. λy. x)

π2 := λp. p (λx. λy. y)

π1 (PAIR a b) => a

π2 (PAIR a b) => b

检查关于Church encoding的 wiki 条目也有一些很好的例子

Answer 2

这个问题的主要主题是了解如何将数据表示为函数。当您使用其他范例时，通常的思维方式是“数据 = 存储在变量中的东西”（可以是数组、对象、任何您想要的结构）。

但是当我们在函数式编程中，我们也可以将数据表示为函数。所以假设你想要一个函数 pair(x,y)

这是“伪”lisp 语言：

(function pair x y = 
   lambda(pick) 
      if pick = 1 return x 
      else return y  )

该示例显示了一个函数，该函数返回一个需要参数的 lambda 函数。

(function pi this-is-pair = this-is-pair 1)

this-is-pair 应该用一个pair函数构造，因此，参数是一个需要其他参数（pick）的函数。

现在，你可以测试你需要的东西

(pi (pair x y ) ) should return x

我强烈建议您观看有关复合数据的视频。大多数示例都是在 lisp 上制作的，但是理解这样的概念很棒。

Answer 3

对或元组描述 Products Domain，是集合 A 的所有元素和集合 B 的所有元素的并集：

A × B = { (a, b) | a ∈ A, b ∈ B }

在这里，A 和 B 是不同的类型，因此，例如，如果您在 C、Java 之类的语言程序中，则可以有对，如(String, Integer), (Char, Boolean),(Double, Double)

现在，函数 π1，只是一个接受一对并返回第一个元素的函数，这个函数通常被调用，这就是first它的样子π1(x, y) = x，另一方面，你有第二个，做同样的事情，但返回第二个元素：

fst(a, b) = a
snd(a, b) = b

当我在大学学习签名“编程语言的特征”时，我们的教授推荐了这本书，请参阅产品领域一章以很好地理解所有这些概念。