如何用程序或 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 中推理，其中块是 BlockClosure 类的对象，我会假设您将要量化的 属性 表示为块 p。

为了简单起见，我们假设属性依赖于一个参数x。那么p(x) 将对应于 Smalltalk 表达式

p value: x

使用参数x 评估块p。

这样，您可以在BlockClosure 类中实现Smalltalk 方法forAll:：

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

它检查接收器块表示的属性p 评估为true对于所有aCollection（您的宇宙）中的元素。

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

forAll: aProperty
  ^aProperty forAll: contents

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