javascript - 如何用过程语言或 OO 语言实现 `forall`(数学)

Question

我正在尝试了解如何使用 Ruby 或 JavaScript 等过程语言或 OO 语言实现 forall。对于 example (这是 Coq):

Axiom point : Type.
Axiom line  : Type.
Axiom lies_in : point -> line -> Prop.
Axiom ax : forall (p1 p2 : point), p1 <> p2 ->
           exists! l : line, lies_in p1 l /\ lies_in p2 l.

我这样做的尝试只是定义一个这样的类(调用 MainAxiom == ax)。

class MainAxiom
  attr :p1
  attr :p2

  def initialize
    raise 'Invalid' if @p1 == @p2
    l = Line.new
    check_lies_in(l, @p1)
    check_lies_in(l, @p2)
  end

  def check_lies_in(line, point)
    ...
  end
end

这有各种各样的错误。它本质上说“对于你用点 p1 和 p2 创建的每个公理，它必须满足在线等属性。”这并不完全符合我的要求。我希望它完成定义实际公理的数学目标。

想知道如何用像 Ruby 或 JavaScript 这样的语言来完成这个，如果不能直接实现的话，尽可能接近。即使它只是一个 DSL 或一个定义某些数据的对象，了解如何作为替代方案也会很有帮助。

首先让我明白的是，attr :p1 和 attr 定义似乎适用于每个实例。也就是说，它似乎在说一些关于 forall 的事情，但我无法准确指出。

也许更像这样的东西更接近:

class MainAxiom
  # forall p1 and p2
  attr :p1 # forall p1
  attr :p2 # forall p2
  attr :line (p1, p2) -> Line.new(p1, p2)

  check_lies_in :p1, :line
  check_lies_in :p2, :line
end

我只想在过程/OO 语言中有任何接近 forall 定义的东西。

Answer 1

如果允许我在 Smalltalk 中进行推理，其中 block 是 BlockClosure 类的对象，我会假设您将要量化的属性表示为 block p。

为简单起见，我们假设该属性取决于一个参数x。然后 p(x) 将对应于 Smalltalk 表达式

p value: x

使用参数 x 计算 block p。

通过这种方式，您可以在 BlockClosure 类中将 Smalltalk 方法 forAll: 实现为:

forAll: aCollection
  aCollection do: [:x | (self value: x) ifFalse: [^false]].
  ^true

检查接收方 block 表示的属性 p 对 aCollection 中的所有元素的计算结果是否为 true >(你的宇宙)。

如果您的 Universe 没有改变(问题上下文中的常见情况)，而改变的是属性，您可以定义类 Universe，它将保存元素的集合在其实例变量 contents 中。然后，您可以在 Universe

中实现

forAll: aProperty
  ^aProperty forAll: contents

其中内部 forAll: 消息是在 BlockClosure 中实现的消息。