Основы теории формальных систем

Введение

Использование аппликативных вычислений при решении разнообразных задач создания программного обеспечения давно признано мощным и полезным подходом к разработке сложных систем. Широкий спектр систем текстовых преобразований, символьных вычислений, систем декларативного программирования основаны на применении механизмов аппликативных вычислений для решения конкретных прикладных задач.

При этом аппликативный подход хорошо формализуем в рамках теории алгоритмов средствами ламбда-исчисления и его специализированного варианта – комбинаторной логики. Наличие строгого математического аппарата позволяет разработчику, с одной стороны, проверить корректность реализации своих моделей, а с другой – обеспечить формальное проектирование новых средств и алгоритмов.

Более того, решение сложных задач часто предполагает использование разнородных языковых средств реализации специализированных подсистем. Предлагаемый подход обеспечивает единую среду вычислений, основанную на совместном использовании общей абстрактной машины и единой объектной системы. Математически обоснованная обобщенная схема трансляции гарантирует корректность реализации каждого языка в рамках интегрированной вычислительной среды.

Таким образом, использование средств аппликативных вычислений при проектировании сложных прикладных систем позволяет разработчику не только получить адекватное решение комплексных задач обработки информации, но и проверить его корректность формальными методами.

Автор выражает благодарность за помощь в создании данного учебного пособия Колычеву В.Д., Гольцеру Ю.Я., Гусаровой Т.Н.

Построение λ- теории

Формально математическую систему можно охарактеризовать с помощью следующих основных компонентов:

• основные символы (алфавит),
• правила образования терминальных символов (утверждений),
• аксиомы,
• правила вывода.

Множество основных символов содержит символы для обозначения констант, операторов и т.д.

В соответствии с правилами образования из этих символов строятся утверждения, затем определяются примитивные утверждения, истинность которых принимается без доказательства (это аксиомы). Далее задаются правила, с помощью которых из справедливых утверждений можно выводить новые справедливые утверждения. Это и есть правила вывода.

Доказательство. Если нужно доказать, что некоторое утверждение в формальной системе истинно, то доказательство представляет собой последовательность утверждений, таких что:

(1) любое утверждение либо является аксиомой, либо его можно получить из одного

или более предыдущих утверждений с помощью правил вывода,

(2) последнее утверждение последовательности является утверждением, которое надо

доказать.

Утверждение, для которого существует доказательство, называется теоремой (Th) этой формальной системы.

Пример. Исчисление высказываний.

1. Алфавит: { (,),→, ¬, а₁ , а₂ ,…},

2.1. Все переменные - а₁,а₂,…, являются утверждениями, т.е. все а_i -утверждения (i=1,2,…).

2.2. Если А, В - утверждения, то ­­­¬А и (А→В)- тоже утверждения.

А – утверждение, В – утверждение =>

(А→В) – утверждения, ¬А - утверждение

2.3. Никакой другой набор символов не является утверждением.

3.1. (А→(В→А));

3.2. ((А→(В→С))→((А→В)→(А→С)));

3.3. ((¬В→ ¬А)→((¬В→А)→В));

Правилом вывода является “схема заключения” (modus ponens), т.е. из утверждений (А→В) и А можно вывести В: (А→В), А.

B

Понятие λ-исчисления.

Существует две точки зрения на понятие функции:

• Операционный взгляд:

Функция представляется алгоритмом, который по заданному значению аргумента возвращает значение функции

• Денотационный взгляд:

Функция представляется графиком или множеством пар (аргумент - значение).

Определение:

λ-исчисление – формальная бестиповая теория, рассматривающая функцию как правило (операционный взгляд).

Построение бестипового λ-исчисления.

1. Алфавит: (,), λ,_i, x₁,…, c₁, ….

мн-во мн-во

переменных констант

2. Правила построения объектов (термов):

2.1. Все переменные и константы – термы;

А - терм, В - терм => (АВ) - терм

А-терм, х- переменная, λ-абстракция => λх.А - терм

3. Никакой другой набор символов не является λ-термом.

Пример. ƒ(х)=х+1

ƒ3= ƒ(3)=3+1

ƒ: λх.х+1

ƒ3=((λх.х+1)3)=3+1.

Соглашение о скобках:

• скобки расставляются по ассоциации влево;
• самые внешние скобки можно убирать.

(АВ)→АВ

(((АВ)С)D) →((АВ)С)D→(АВ)СD→ABCD

Соглашение о λ-символах:

Несколько последовательных абстракций можно объединять одним символом λ:

λx. λy. A = λxy.A

3.Аксиомы λ- исчислений:

(α) λу.z= λυ.[υ/y]z (подстановка υ на место у в выражении z).

Связанные переменные в выражении можно переименовывать.

λх.х+1=^(α) λу.у+1

(β) (λх.M)N=[N/x]M

(ρ) M=M

4.Правила вывода:

(μ) x=y→ ax=ay

(ν) x=y→ xa=ya

(ξ) a=b→ λx.a=λx.b

(τ) a=b, b=c→ a=c

(σ) a=b→ b=a

Постулаты λ - исчисления - все аксиомы и правила построения.

Примеры: х а @ b – не является λ-термом.

λх.у

λх.у→((λх.х)3)

Дата добавления: 2014-01-11