close

Вход

Забыли?

вход по аккаунту

?

λ исчисление - Yauhen Yakimovich

код для вставкиСкачать
Функции
λ исчисление
Eugeny L Yakimovitch http://desk.by/~ewger 2008
Алонзо Чёрч (1903 - 1995)
Автор теории
лямда-исчислений
Проблема останова и
исследование разрешимости
вычислительных задач
Тезис Чёрча (Тьюринга-Чёрча)
Теорема Чёрча
Хроника формализации
Использование индийских чисел
Абу Абдуллах Мухаммеда ибн Муса
аль-Хорезми: Китаб аль-джебр вальмукабала «Книга о сложении и
вычитании»
Математические уравнения
оформленные Франсуа Виетом
(1540—1603) .
Хроника формализации
Виет ввел в математическое
использование символьные выражения и
уравнения в современной форме
Потребовалось еще 250 лет до разработки
нотации условных функций, предложенной
Чёрчем
Основные ЯП поддерживающие
лямда функции
Lisp
ML
Haskell
OCaml
Источники литературы
Henk Barendregt, Erik Barendsen Introduction to
Lambda Calculus
Achim Jung, A Short Introduction to the Lambda
Calculus
Raúl Rojas, A Tutorial Introduction to the
Lambda Calculus
Peter Selinger, Lecture Notes on the Lambda
Calculus
The Lambda Calculus, notes by Don Blaheta.
October 12, 2000
Особенности λ исчисления
Простая форма записи сложных
вычислений
Является полноценным универсальным
языком программирования
Эквивалентно машине Тьюринга
λ - выражения
На бесконечном множестве имен
переменных, λ – выражение является
результатом следующего правила BNF
подстановки:
<expr> := <name>|<function>|<application>
<function> := λ <name>.<expr>
<application> := <expr><expr>
(продолжение)
Для простоты выражения можно
заключать в скобки
(1)
E = (E)
Единственные ключевые слова
универсального языка это символы
точки «.» и греческой лямбды «λ»
Тождество
x.x
(2)
(x.x) y [ y / x]x y
(3)
x.x y. y t.t u.u
(4)
Свободные и связанные
переменные
(x.xy)
(5)
(x.x)(y. yx)
(6)
В (5) λ выражении x связанная, а y несвязанная
(свободная) переменная. В (6) формуле в первом
λ выражении слева x связан c первой λ, а в теле
второго λ выражения y – связанная, x – не
связанная переменные.
Числительные Чёрча
0 sz.z s.(z.z ) (7)
1 (sz.s ( z ))
(8)
2 (sz.s ( s ( z )))
(9)
3 (sz.s ( s ( s ( z ))))
(10)
Функция приемника
S wyx. y ( wyx)
(11)
S 0 (wyx. y ( wyx))( sz.z )
(12)
(yx. y (( sz.z ) yx)) yx. y (( z.z ) x) yx. y ( x) 1
S1 (wyx. y ( wyx))( sz.s ( z )) yx. y ((sz.s ( z )) yx)
yx. y ( y ( x)) 2
(13)
Булевская логика
true=λab.a
false=λab.b
not p=(p)(false)(true)
a and b=(a)(b)(false)
a or b=(a)(true)(b)
a xor b=(a)((b)(false)(true))(b)
Проверка условий
Z x.xFF
0 fa (sz.z ) fa 0
Fa (xy. y ) a y. y I
Функция приемника
(z.zab )
(z.zab )T Tab a
(z.zab ) F Fab b
(pz.z (S( pT ))( pT ))
P (n.n (z.z 00) F
Рекурсия : Y Комбинатор
Yf f(Yf)
Y f g f gg g f gg Yf g f gg g f gg f g f gg g f gg Числа, проекция, нуль
Числа могут быть представлены в виде
стандартны числительных Чёрча
Проекция функций возвращает
единственное число из кортежа
p ( x1 x2 ..xn ) xi x1 x2 ..xn .xi
n
i
Функция нуля возвращает нулевое
значение для любых параметров
z ( x1 x2 ..xn ) 0 x1 x2 ..xn .zero
n
i
Кортежи
pair = λabf.fab
first = λp.p(λab.a)
second = λp.p(λab.b)
Списки
empty = λfx.x
append = λalfx.fa(lfx)
head = λl.l(λab.a)(any expression)
isempty = λl.l(λab.true)false
tail=λl.first(l(λab.pair(second b)(append a
(second b)))(pair empty empty))
Композиция
f( g1(x1,x2,…,xm),
g2(x1,x2,…,xm),
…,
gn(x1,x2,…,xm))
Примитивная рекурсия
ρn(f,g) есть функция h такая что:
h(x1,x2,…,xn,0) = f(x1,x2,…,xn)
h(x1,x2,…,xn,x+1) =
g(x1,x2,…,xn,x,h(x1,x2,…,xn,x))
Минимизация
μ(f)(x1,x2,…,xn) возвращает наименьший
x при котором f(x1,x2,…,xn,x)=0 (такой x
может не существовать).
Теорема Чёрча-Россера
Если A B существует выражение C ,
такое что A => C и из B => C
Следствие: Нормальная форма для
нормированного выражения уникальна.
Документ
Категория
Презентации
Просмотров
25
Размер файла
342 Кб
Теги
1/--страниц
Пожаловаться на содержимое документа