Проверка достоверности доказательства в Идрисе

Я пытаюсь написать тестовый код, чтобы проверить, действительно ли plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a доказывает a + b = b + a на натуральных числах, то есть код не подделывает их, используя типизированные отверстия, postulate, believe_me, assert_total и т. д.

В частности, если доказательство каким-то образом сфальсифицировано, я хочу, чтобы программа потерпела неудачу одним из трех способов:

  • Ошибка компиляции
  • Ошибка времени выполнения, например. сегментация
  • Бесконечный цикл во время выполнения

Если эти варианты неосуществимы, я открыт для анализа исходного кода в качестве крайней меры (для моих целей это также должно быть написано на Idris). Я слышал о Language.Reflection, но не уверен, что это правильный инструмент.

Приведенный ниже код — это одна неудачная попытка, потому что proofEval даже не смотрит на фактическое переданное значение:

plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a
plusComm a b = ?plusComm

proofEval : {a : ty} -> (a = b) -> ty
proofEval {a=a} _ = a

main : IO ()
main = do
  putStrLn "Compiled Successfully!"
  print (proofEval (plusComm 1 2))

Вышеупомянутое, когда скомпилировано и запущено, выдает следующий вывод и завершает работу без ошибок.

Compiled Successfully!
3

testing theorem-proving idris
person Bubbler    schedule 09.03.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Частичный ответ

I found a способ поймать postulate и дыры с помощью зависимых кортежей:

plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a
plusComm = plusCommutative

proofEval : (a : Nat) -> (b : Nat) -> (a : Nat ** (b : Nat ** (a + b = b + a)))
proofEval a b = (a ** (b ** plusComm a b))

main : IO ()
main = do
  putStrLn "Compiled Successfully!"
  print $ fst $ snd $ proofEval 1 2
  -- `print $ fst $ proofEval 1 2` doesn't work for the purpose

Выход:

Compiled Successfully!
2

Некоторые возможные поддельные доказательства и результаты:

-- typed hole
plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a
plusComm = ?plusComm
-- result: runtime error (abort)
ABORT: Attempt to evaluate hole Main.plusComm1

-- postulate
postulate plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a
-- result: compilation error
reachable postulates:
  Main.plusComm

Обратите внимание, что assert_total или believe_me не перехватывается с помощью этого метода, как указано в связанном фрагменте.

person Bubbler    schedule 10.03.2019