如何用程序或OO语言实现`forall`（数学） [英] How to implement `forall` (mathematics) in a procedural or OO language

问题描述

我试图了解如何在程序或OO语言（如Ruby或JavaScript）中实现 forall 。对于示例（这是Coq）：

I am trying to understand how to implement forall in a procedural or OO language like Ruby or JavaScript. For example (this is 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.

我这样做的尝试只是定义一个这样的类（call MainAxiom == ax ）。

My attempt at doing this is just defining a class such as this (call 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创建的每个公理，它必须满足在一条线上的属性等等。这并不是我想做的事情。我希望它能够实现定义实际公理的数学目标。

This has all kinds of mistakes. It essentially says "for every axiom that you create with points p1 and p2, it must satisfy the properties of being on a line, etc.." This doesn't quite do what I want it to do. I want it to accomplish the mathematical goal of defining an actual axiom.

想知道如何用Ruby或JavaScript这样的语言实现这一目标，如果它是尽可能接近的话不是直接可能的。即使它只是一个DSL或定义某些数据的对象，这将有助于知道如何做替代。

Wondering how to accomplish this in a language like Ruby or JavaScript, something as close to as possible if it's not directly possible. Even if it's just a DSL or an object defining some data, that would be helpful to know how to do as an alternative.

第一部分让我知道， attr：p1 和attr定义似乎适用于每个实例。也就是说，似乎说了一些关于 forall 的内容，但我无法指出它。

The first part that gets me is that, the attr :p1 and attr definitions seem to apply to every instance. That is, it seems to say something about forall, but I can't pinpoint it.

也许这样的事情更接近：

Maybe something more like this is closer:

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 定义的一半。

I just want to have anything even halfway close to a forall definition in a procedural/OO language.

推荐答案

如果我允许在Smalltalk中推理，其中块是类的对象 BlockClosure ，我认为你代表属性你要量化为块 p 。

If I'm allowed to reason in Smalltalk, where blocks are objects of the class BlockClosure, I would assume that you represent the property you want to quantify as a block p.

为简单起见，我们假设该属性依赖于一个参数 x 。然后 p（x）将对应于Smalltalk表达式

For the sake of simplicity let's assume that the property depends on one single parameter x. Then p(x) would correspond to the Smalltalk expression

p value: x

评估块 p 使用参数 x 。

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

In this way, you could implement the Smalltalk method forAll: in the class BlockClosure as:

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

检查属性 p 评估为 true 所有 aCollection中的元素（您的宇宙）。

which checks that the property p represented by the receiver block evaluates to true for all the elements in aCollection (your universe).

如果您的Universe没有变化（在问题的上下文中通常的情况），以及该属性的变化，您可以定义类 Universe ，它将在其实例变量 contents 中保存元素集合。然后，您可以在 Universe中实现

If your universe doesn't change (the usual case in the context of a problem), and what changes is the property, you could define the class Universe, which would hold the collection of elements in its instance variable contents. Then, you could implement in Universe

forAll: aProperty
  ^aProperty forAll: contents

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

where the inner forAll: message is the one implemented in BlockClosure.

这篇关于如何用程序或OO语言实现`forall`（数学）的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！