2

我试图了解如何用forallRuby 或 JavaScript 等过程或 OO 语言来实现。例如（这是 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

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

4

1 回答 1

1

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

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

p value: x

p它使用参数评估块x。

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

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

它检查由接收器块表示的属性是否针对（您的宇宙）中的所有元素p进行评估。true aCollection

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

forAll: aProperty
  ^aProperty forAll: contents

其中内部forAll:消息是在BlockClosure.

于 2019-03-03T02:52:21.517 回答