Сошников Дмитрий Валерьевич к.ф.-м.н., доцент Сошников Д.В. Факультет инноваций и высоких технологий Московский физико-технический институт

2 Лекция 14 Введение в -исчисление

©2008 Сошников Д.В. 3 Для понимания возможностей и ограничений программирования необходимо представлять себе, что можно запрограммировать, а что нельзя Необходима формальная математическая модель процесса вычислений Модель позволяет рассуждать, доказывать теоремы и т.д.

©2008 Сошников Д.В. 4 Машина Тьюринга Попытка смоделировать простейшую вычислительную машину Математически громоздкая, но приближенная к реальности λ-исчисление / рекурсивные функции Формальная аксиоматическая система, изучающая свойства функций, их вызовов, композиций и описаний Математически привлекательная, но необходимы усилия, чтобы показать согласованность с традиционной архитектурой ЭВМ

©2008 Сошников Д.В. 5 Алгоритмы Маркова Простейшие правила переписывания и сопоставления с образцом В основе языка программирования Рефал Логика предикатов / метод резолюций Попытка сформулировать определение вычисления начиная от постановки задачи в терминах естественного логического описания

©2008 Сошников Д.В. 6 Формальная аксиоматическая система Синтаксис (ППФ) Аксиомы Правила вывода Семантика Прагматика

©2008 Сошников Д.В. 7 Чистое λ-исчисление Изучает возможности описания и комбинирования функций, не наделенных семантикой В рамках чистого λ-исчисления возможно построить объекты для моделирования чисел, списков и т.д. Прикладное λ-исчисление Чистое λ-исчисление пополняется некоторым набором объектов-констант и соответствующих правил вывода

©2008 Сошников Д.В. 8 Алфавит: {a,b,…} {λ,(,),.} ППФ: ::= | ( ) | | λ. | λ. - абстракция - аппликация

©2008 Сошников Д.В. 9 ABC = ((AB)C) λxy. = λx.λy. = λx.(λy. ) Область действия λ распространяется максимально вправо Таким образом (λxy.f x y) a b = (λy.f a y) b = f a b

©2008 Сошников Д.В. 10 Свободные переменные в формуле – переменные, не находящиеся под знаком λ FV(expr) – определяется рекурсивно FV( ) = {id} FV( )=FV( ) FV( ) FV(λx. ) = FV( )\{x} BV(expr) – связанные переменные Var(expr) – множество всех переменных

©2008 Сошников Д.В. 11 Замену переменной x на выражение А в выражении E будем обозначать [A/x]E Определяется рекурсивно: [A/x] =, если x [A/x]x = A [A/x](e 1 e 2 )=([A/x]e 1 ) ([A/x]e 2 ) [A/x] λy.E = λy. [A/x] E [y/x] λx.E = λy. [y/x] E, y FV(E)

©2008 Сошников Д.В. 12 -преобразование Замена связанной переменной в абстракции λx.E λy.[y/x]E, y Var(E) β-преобразование Применение абстракции (λx.E)A β [A/x]E, где x BV(E) Преобразование называется редукцией, если оно ведет к упрощению выражения

©2008 Сошников Д.В. 13 (λf.λx.f 4 x) (λy.λz.+ z y) 3 Здесь + использован как допустимый символ для ясности (λf.λx.f 4 x) (λy.λz.+ z y) 3 β (λx. (λy.λz. + z y) 4 x) 3 β (λy.λz.+ z y) 4 3 β (λz.+ z 4) 3 β Возможен другой путь редукции: (λf.λx.f 4 x) (λy.λz.+ z y) 3 β (λx. (λy.λz. + z y) 4 x) 3 β (λx. (λz. + z 4) x) 3 β λx. (+ x 4) 3 β Оба пути приводят к одинаковому результату Подчеркнутая часть – к которой применяется правило редукции - редекс

©2008 Сошников Д.В. 14 Рассмотрим λx.(λx.x)(+ 1 x) x в подчеркнутом выражении – это «другой» x (λx.(λx.x)(+ 1 x)) 1 β (λx.1)(+ 1 1) β 1 Неправильная редукция, из-за конфликта имен! (λx.(λx.x)(+ 1 x)) 1 α (λx.(λt.t)(+ 1 x)) 1 β (λt.t)(+ 1 1) β (+ 1 1)