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

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

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

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

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

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

(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

            λх.у

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