How to implement `forall` (mathematics) in a proce

问题:

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.

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

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.

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.

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

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

回答1:

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.

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

which evaluates the block p using the argument x.

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

which checks that the property p represented by the receiver block evaluates to true for all the elements in aCollection (your 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

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