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.

これを行う私の試みは、このようなクラスを定義するだけです (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で作成するすべての公理について、線上にあるなどのプロパティを満たさなければならない..」と言っていますが、これは私がやりたいことではありません。実際の公理を定義するという数学的目標を達成したいと考えています。

Ruby や JavaScript などの言語でこれを実現する方法を知りたいのですが、それが直接可能でない場合は、可能な限り近いものを作成してください。それが単なる DSL やデータを定義するオブジェクトであっても、代わりの方法を知っておくと役に立ちます。

最初に気になったのは、attr :p1and 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手続き型/オブジェクト指向言語の定義に半分でも近いものが欲しいだけです。

4

1 に答える 1