forall
Ruby や 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 :p1
and 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
手続き型/オブジェクト指向言語の定義に半分でも近いものが欲しいだけです。