Как реализовать `forall` (математику) на процедурном или оо-языке - PullRequest
Новая
       68

Как реализовать `forall` (математику) на процедурном или оо-языке

0 голосов
/ 01 марта 2019

Я пытаюсь понять, как реализовать forall на процедурном или OO-языке, таком как Ruby или JavaScript.Для пример (это 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-языке.

1 Ответ

0 голосов
/ 03 марта 2019

Если мне разрешено рассуждать в Smalltalk, где блоки являются объектами класса BlockClosure, я бы предположил, что вы представляете свойство , которое вы хотите измерить как блок p.

Для простоты предположим, что свойство зависит от одного параметра x.Тогда p(x) будет соответствовать выражению Smalltalk 

p value: x

, которое оценивает блок p, используя аргумент x.

Таким образом, вы можете реализовать метод Smalltalk forAll: в классе BlockClosure как: 

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

, который проверяет, что свойство p, представленное блоком получателя, оценивается как true для всех элементов в aCollection (ваша вселенная).

Если ваша вселенная не меняется (обычный случай в контексте проблемы), и какие изменения это свойство, вы можете определить класс Universe, который будет содержатьколлекция элементов в переменной экземпляра contents.Затем вы можете реализовать в Universe

forAll: aProperty
  ^aProperty forAll: contents

, где внутреннее сообщение forAll: - это сообщение, реализованное в BlockClosure.

.
...