Введение

Это моя программа для формальной верификации математических доказательств, она же proof assistant. Программа пока не имеет названия, есть только рабочее название "pa" (сокращение от "proof assistant").

Итак, работа с программой происходит так: человек берёт какое-нибудь математическое доказательство, затем самостоятельно записывает это доказательство в формальном виде, т. е. на языке, пригодном для проверки компьютером. Затем это доказательство подаётся на вход моей программе и она сообщает, верно доказательство, или нет.

Моя программа относится к классу proof assistant'ов, т. е. программ для верификации доказательств. Моя программа далеко не единственная в этом классе, есть полно других proof assistant'ов, например, Isabelle и Coq. Тем не менее, я начал писать свой proof assistant, т. к. все сущетвующие proof assistant'ы, на мой взгляд, имеют недостатки, и я собираюсь написать proof assistant, который будет лучше их всех :).

На данный момент моя работа над программой только началась. Версия, которую вы сейчас видите, написана на C++, я уже начал переписывать свою программу на Haskell'е, попутно внося изменения по существу, но Haskell-версия пока не работает, поэтому здесь я её не выкладываю. Почему же я тогда вообще выкладываю программу, раз работа только началась? Для удобства ссылок. Т. е. если я кому-нибудь скажу, что пишу proof assistant, я могу дать ему ссылку на этот проект на Github'е.

Честно говоря, это не proof assistant, а proof checker, т. к. нет интерактивности. Но я всё равно буду называть программу "proof assistant", т. к. я так привык

Установка и запуск программы

Работоспособность программы проверялась только на GNU/Linux, так что инструкции будут только для этой системы (хотя теоретически должна поддерживаться любая система, включая Windows). Программа зависит от моей библиотеки libsh (http://github.com/safinaskar/libsh ), инструкции по её установке тоже будут даны ниже. Теперь нужно выполнить следующие инструкции, они будут включать скачивание и установку libsh и pa.

Итак, установите все зависимости (wget, git, g++, make, cmake, flex, bison версии, по всей видимости, как минимум 3.0.3, и он должен быть установлен в /opt/bison-3.0.3), затем:

$ wget https://github.com/safinaskar/libsh/releases/download/v0.1.0/libsh-extended-0.1.0.tar.gz
$ tar -xf libsh-extended-0.1.0.tar.gz
$ mkdir libsh-build
$ cd libsh-build
$ cmake -DCMAKE_INSTALL_PREFIX=/usr/local ../libsh-0.1.0
$ make
$ sudo make install
$ cd ..
$ git clone git@github.com:safinaskar/pa-0.1.git
$ cd pa-0.1
$ make

Теперь в текущей папке лежит бинарник pa, это и есть моя программа. Запускать её нужно так:

$ ./pa < file

где file - это файл с формальным текстом. Если программа ничего не выдала, значит, ошибок нет. В противном случае выдаётся текст ошибки. В каталоге вместе с исходными текстами лежит файл test.sh с примерами формального кода. Его можно использовать для тестирования программы. Запускать так:

$ ./test.sh ./pa

Иными словами, нужно передать к test.sh в качестве аргумента бинарник моей программы. test.sh создаст кучу формальных текстов в текущей папке и запустит на них мою программу.

make clean не предусмотрено. Чтобы удалить сгенерированные файлы, наберите git clean -x -f -d (осторожно! Это удалит все файлы, кроме находящихся в git'е).

Формальный язык

Язык моей программы похож на язык Isabelle. Программа не привязана ни к какой конкретной логике, такой как классическая логика, интуиционистская, логика первого порядка, второго и т. д. Вместо этого поддерживается так называемый logical framework, т. е. возможность задать любую логику. В примерах в test.sh показано, как с нуля построена классическая логика, затем логика первого порядка, логика с равенством и аксиоматика Пеано. Язык достаточно мощен, чтобы сформулировать теорему о полной индукции и вывести её из аксиом Пеано (есть в примерах). Базовой логикой является HOL (higher order logic, логика высшего порядка). Никаких логических связой, поддерживаемых "с нуля", нет.

Вообще, если вы хотите понять мою программу, то нужно сперва изучить азы матлогики, например, по лекциям Беклемишева (http://lpcs.math.msu.su/vml2010 ), а затем поработать в Isabelle (текущая версия моей программы очень похожа на Isabelle).

Итак, ещё разок, про мой формальный язык. Это типизированная логика высшего порядка с лямбда-выражениями. Терм представляет собой переменную, константу, терм, применённый к терму, либо лямбда-выражение. Разделения между термами и формулами нет. То, что в других языках называется формулой - у меня просто терм типа prop, который является обычным типом (за исключением того, что этот тип встроенный, т. е. его не надо объявлять). Изначально объявлен лишь один тип (prop) и ни одной константы (в том числе ни одной логической связки).

Что, собственно, я хочу? Я хочу язык с синтаксисом и удобством, как у Isabelle, но с поддержкой доказательств-как-термов как у Coq. В идеале ответить на все вопросы поставленные здесь: http://www.cs.ru.nl/~freek/talks/lsfa.pdf .

Я думаю, не нужно пояснять, что test.sh - это shell-скрипт, что его первые строчки - это код на shell, а вот всё, что находится между cat ... и EOF (таких фрагментов много) - это код уже на самом формальном языке.

Автор: Аскар Сафин, safinaskar@mail.ru, http://vk.com/safinaskar

Лицензия: GPLv3