LCME Пятница, 26.05.2017, 00:50
Главная | Регистрация | Вход Приветствую Вас Гость | RSS
[ Новые сообщения · Участники · Правила форума · Поиск · RSS ]
Страница 1 из 11
Форум » Билеты к экзаменам » Программирование » 02 Бета-редукция
02 Бета-редукция
freidomДата: Воскресенье, 27.12.2009, 17:16 | Сообщение # 1
Главный тут
Группа: Администраторы
Сообщений: 273
Репутация: 20
Статус: Offline
Свобода для подстановки. Бета-редекс и бета-редукция. Формальное и неформальное определения. Нормальная форма.

Запись A[x:=B] обозначает такой терм C, полученный из терма A, что в нём все свободные вхождения переменной x заменены на B. Эта операция называется подстановкой.
То же самое более формально:

Code
let rec replace a x b =
  if (not (x /- (fv a))) then a else (
  match a with
    _ when not (x /- (fv a)) -> a
   |Var _ -> b
   |App (p, q) -> App (replace p x b, replace q x b)
   |Abs (v, r) -> Abs (v, replace r x b)
   |Nil -> Nil );;

Это вариант Штукенберга, http://lcme.ucoz.ru/_fr/1/5670364.jpg . Очень странное определение. Не проще ли пройтись по всему лямбда-терму A в поисках переменной x, вместо того чтобы каждый раз вычислять список свободных переменных?

Перед определением бета-редукции нам понадобится ещё одна функция, возвращающая контекст подстановки переменной в лямбда-выражение, иными словами, список всех переменных, связанных в местах подстановки данной переменной.

Code
let cx y z =
  let rec cx' a x =
   match a with
     _ when not (x /- (fv a)) -> []
    |Var v -> []
    |App (b, c) -> unite (cx' b x) (cx' c x)
    |Abs (b, c) -> b::(cx' c x)
    |Nil -> []
  in unique (cx' y z);;

Бета-редексом называется выражение вида (\x.A) B.
Бета-редукцией бета-редекса (\x.A) B называется терм A[x := B]. При этом требуется, чтобы cx (A, x) /\ fv (b) = 0, иначе результат бета-редукции не определён (пока). Это условие необходимо для того, чтобы никакое свободное вхождение переменной в B не стало связанным после бета-редукции.
Если результат редукции не определён, то прежде проведения редукции следует провести переименование переменных, связанных в терме A, иными словами, найти такой терм C, что C @= A и cx (C, x) /\ fv (B) = 0.
Бета-редукцией произвольного выражения называется операция редукции произвольного редекса, вложенного внутрь этого выражения, либо, если такового нет, то возврат самого выражения.

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

 
Форум » Билеты к экзаменам » Программирование » 02 Бета-редукция
Страница 1 из 11
Поиск:

Copyright Freidom © 2017 Хостинг от uCoz