Рекурсия. Рекурсивное определение- это определение, которое внутри себя содержит ссылку

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

Рекурсивное определение - это определение, которое внутри себя содержит ссылку

на определяемый объект.

Пример. 1) Факториал ƒac(x): x*ƒac(x-1),

if (х=0) then 1 ƒac(0)=1.

else x* ƒac(x-1)

2) Список:

Голова

cons(x.y)→(x.y) (точечная пара)

head(x.y) →x (голова)

nil

tail(x.y) → y (хвост)

length(x)

tail(x) = Nil

length(x) = 1+ length(tail(x))

length(x): if x = Nil then 0

else 1+(length(tail(x))).

Рекурсия в λ-исчислении.

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

Выражение х является неподвижной точкой функции ƒ, если х = ƒх.

Теорема: (О неподвижной точке).

1)Для

2) -позволяет определить неподвижную точку.

↑обьект ↑неподвижная точка

Пример. Y = λƒ.(λx.ƒxx)(λx.ƒxx)

YH = …H(YH)

# w = λx.ƒxx – введем этот объект и скажем, что х = ww =

┌──_↓─_↓

= (λх.ƒ(x x))(λx.ƒ(xx)) = ƒ((λx.ƒ(xx))(λx.ƒ(xx))) = ƒ(x) 1) доказано. #

↑

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

Комбинатор неподвижной точки - это терм М: , т.е. Мƒ - неподвижная точка.

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

Пример. θ = (λxу.(у(хху))(λxу.у(хху))

С помощью комбинатора Y запишем и вычислим комбинатор какого-либо числа.

ƒac: λx.(if x=0,1,x* ƒac(-x1)) (λx.IF(=x0)1(*ƒac(-x1))

Вычислим факториал от 2: ƒac= λx.(… ƒac …).

Применяя λ - абстракцию, получим ƒac(2) λƒac1.ƒacƒac1= (λƒac1.(λх.(… ƒac1…)))ƒac

Введем дополнительную функцию H, которая в определении факториала позволяет абстрагироваться от определения факториала.

По правилу (η) λƒac1.ƒacƒac1=ƒac и ƒac= λƒac1.(λх.(…ƒac1…)))ƒac.

H=λƒac1.(λх.(IF x=0,1,x*ƒac1(-x1))

ƒac=Hƒac YH=H(YH)

ƒac2=YH2

Шаг за шагом произведем эти вычисления.

┌───_↓─────_↓

(λƒ.(λх.ƒхх)(λх.ƒхх))(λƒac.(λn.(if n=0,1,n*ƒac(n-1))))2((λƒac.(λn.(if n=0,1,

n*ƒac(n-1))))(YH))2(λn.(if n=0,1,n*(YH)(n-1)))2 if (2=0),1,2*(YH)(2-1)

2*((YH)1) 2*[H(YH)1] 2*[(λƒac.λn.if n=0,1,n_*ƒac(n-1))(YH)1]

2*[ if 1=0,1,1*(YH)(1-1)] 2*[1*(YH0)] 2*1*(YH0)

2*1*[H(YH)0] 2*1*[(λƒacn.if n=0,1,n_*ƒac(n-1))(YH)0]

2*1*[ if 0=0,1,n*[(YH)(0-1)]] 2*1*1=2.

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

Бестиповое λ - исчисление является синтактико-семантической системой, т.е. семантика выражения полностью определяется его синтаксисом.

Синтаксис - способ записи выражения.

Семантика – смысл выражения. Алгоритм вычисления выражения полностью определяется способом его записи.

Все вычисления в символьных системах сводятся к подстановке одних идентификаторов вместо других, при этом они вначале вычисляются в среде, результат вычисления выражения изменяет исходную среду на новую.

Контрольные вопросы

1. Дайте определение формальной системы.
2. Приведите примеры символов и термов в λ–исчислении.
3. На основании каких постулатов λ–исчисления можно избавиться от коллизии переменных?
4. Какие аксиомы и правила вывода λ–исчисления позволяют применить функцию к ее аргументам?
5. На основании каких положений доказывается единственность нормальной формы?
6. С помощью каких средств могут быть заданы алгоритмы, использующие примитивную рекурсию?

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