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

Введение

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

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

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

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

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

 

 

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

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

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

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

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

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

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

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

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

доказать.

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

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

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

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

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

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

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

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

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

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

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

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

B

 

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

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

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

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

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

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

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

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

 

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

  1. Алфавит: ( , ) , λ ,i , x1,… , c1, … .

мн-во мн-во

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

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)