Русскоязычное программирование

Информация о пользователе

Привет, Гость! Войдите или зарегистрируйтесь.


Вы здесь » Русскоязычное программирование » система типов » Автоматизация доказательств


Автоматизация доказательств

Сообщений 1 страница 5 из 5

1

Coq and Agda are automated theorem provers that use dependently typed lambda calculus as a basis

https://ru.wikipedia.org/wiki/Автоматическое_доказательство

Процесс доказательства основывается на логике высказываний и логике предикатов.

после полной автоматизации доказательство называют уже "вычислением".

В настоящее время автоматическое доказательство теорем в промышленности применяется в основном при разработке и верификации программного обеспечения.

Корпорация Microsoft использует автоматический доказатель теорем Z3 для верификации кода операционной системы Windows и других программных продуктов

The typed lambda-calculus is a formulation of higher-order logic well suited to the formalization of mathematics and other disciplines.

one can search for a proof of a theorem of typed lambda-calculus by searching for an expansion proof which expresses the fundamental logical structure of the theorem, and then transform this into a proof in natural deduction style.

https://en.wikipedia.org/wiki/%CE%9BProlog

There is currently a great deal of research into lambda calculus by the programming language, theorem proving and symbolic computing communities.
https://www.math.cmu.edu/math/faculty/StatmanRichard

mathematical expressions and statements can be modeled using lambda calculus.

The lambda calculus is also a logic. It was originally created to solve one of the many early formulations of the halting problem. It turned out, though, that the raw untyped lambda calculus allowed for unrestricted recursion (the fixedpoint combinators), making it unsuitable for logic (turing completeness in a logic makes your logic inconsistent. The liar's paradox is just an infinite loop).
To fix this problem, Church revised the lambda calculus, adding types to it. The "simply typed" lambda calculus restrict the expressivity of the language severely, but kept it consistent.

(Специально для Уткина - количество использованного английского языка является индикатором уровня моего непонимания вопроса. Чем лучше понимаю, тем больше обхожусь своими словами)

Отредактировано Лис (2018-01-30 18:48:00)

0

2

Корпорация Microsoft использует автоматический доказатель теорем Z3 для верификации кода операционной системы Windows и других программных продуктов

Да брешут они как сивые мерины. Количество ошибок в винде зашкаливает. В других их тоже полно, но они хотя бы так нагло не врут :).

0

3

utkin написал(а):

Да брешут они как сивые мерины.

Надо понимать, что под этим подразумевается формальная корректность записи кода с точки зрения некоторой ограниченной грамматики.
Как, например, и корректность, синтаксиса программы. Будет ли она при этом работать правильно? Ответить на этот вопрос невозможно. Так как нужна сверка кода программы с поставленной на человеческом языке задачей, а такое Microsof не умеет.
Но можно добиться, например, чтобы ОС никогда не впадала в отдельные недопустимые состояния при отсутствии некоторых аппаратных сбоев, или наоборот, справлялась с некоторыми из них.

Отредактировано MihalNik (2018-01-30 21:58:22)

0

4

Ну и смысл в таком автоматном доказательстве?

Но можно добиться, например, чтобы ОС никогда не впадала в отдельные недопустимые состояния при отсутствии некоторых аппаратных сбоев, или наоборот, справлялась с некоторыми из них.

А, то есть без такой проверки ОСь бы вообще не запускалась :). Ясно.

0

5

utkin написал(а):

А, то есть без такой проверки ОСь бы вообще не запускалась

Или вела бы себя непредсказуемо, с ранними версиями так и было. Ну также как с компиляцией - по ограниченной грамматике идёт дополнительная избыточность, проверка защищает от простейших ошибок вроде некоторых опечаток. Т.е., например, такую грамматику, защищающую от опечаток некоторой плотности, построить можно. Вот и проверка правильности работы ограниченной части некоторого автомата - вполне программируемая задача.

Отредактировано MihalNik (2018-01-31 11:39:59)

0


Вы здесь » Русскоязычное программирование » система типов » Автоматизация доказательств