Для изучения зависимых типов я переписываю свою старую игру на Haskell в Idris. В настоящее время «движок» игры использует встроенные целочисленные типы, такие как Word8. Я хотел бы доказать некоторые леммы, касающиеся числовых свойств этих чисел (например, что двойное отрицание является тождеством). Однако ничего нельзя сказать о поведении примитивных арифметических операций. Что было бы лучше, просто использовать believe_me или другое ручное махание (по крайней мере, для самых основных свойств), или переписать мой код, используя Nat, Fin и другие «высокоуровневые» числовые типы?
Примитивные операции в доказательствах
Ответы (2)
Я бы предложил использовать postulate для любых необходимых вам примитивных свойств, стараясь, конечно, использовать только те вещи, которые на самом деле верны для рассматриваемых числовых типов (что в основном просто означает осторожность в отношении переполнения). Таким образом, вы можете сказать что-то вроде:
postulate add_commutes : (x, y : Int) -> x + y = y + x
believe_me лучше избегать, если вам не нужно какое-то вычислительное поведение доказательства. Но, если честно, мы все еще пытаемся разобраться в этом, когда рассуждаем о примитивах...
person
Edwin Brady
schedule
09.06.2015
Я считаю, что на данный момент лучше использовать Nat, когда это возможно. Разработчики Idris планируют, в конце концов, реализовать общий механизм замены удобных для доказательства типов быстрыми примитивными при компиляции, но пока это происходит только для Nat. Вы могли бы believe_me пройти, если бы действительно хотели, но в итоге вы получили бы функции, с которыми не так просто работать в доказательствах. Обратите внимание, что если вы решите поиграть с believe_me, то вам следует рассмотреть также really_believe_me, что, по-видимому, делает его более правдоподобным для средства проверки типов.
person
dfeuer
schedule
08.06.2015
