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

Лямбда-выражения задаются простой грамматикой. Для её определения сначала введём множества терминальных (At = {"\", ".", "(", ")", <var>}, по традиции, под <var> подразумевается некоторая маленькая буква латинского алфавита) и нетерминальных (An = {"L"}) символов. Тогда грамматика будет выглядеть следующим образом:

L := <var> | \<var>.L | L L | (L)

К сожалению, данное определение обладает существенным недостатком. С его помощью некоторые выражения можно получить несколькими способами.

x x x = x L = L x

Поэтому, хотя такая грамматика и проста для понимания, она требует некоторого усовершенствования. Рассмотрим ещё два варианта.

An = {"L", "app", "term"}

L := [app ] \<var>.L | app
app := [app ] term
term := (L) | <var>

L := \<var>.L | app
app := term L | term
term := (L) | <var>

Обе эти грамматики выглядят вполне правдоподобно, более того, они позволяют разобрать любое лямбда-выражение единственным способом.

 
freidomДата: Воскресенье, 27.12.2009, 16:30 | Сообщение # 2
Главный тут
Группа: Администраторы
Сообщений: 273
Репутация: 20
Статус: Offline
Связанные, связывающие и свободные вхождения переменных.
- в абстракцию \x.A вхождение переменной x называется связывающим;
- в абстракции \x.A любые вхождения переменной x в выражение A называются связанными, кроме тех, которые являются связывающими
- вхождения всех остальных переменных называются свободными

Рассмотрим более формальную иллюстрацию на OCaml. Сначала определим тип лямбда-выражений.

Code
type lambda = Var of string | App of lambda * lambda | Abs of string * lambda;;

Нам понадобится функция для объединения списков с удалением одинаковых элементов.

Code
let ( /- ) = List.mem;;
let unite a b = a @ (List.filter (fun x -> not (x /- a)) b);;

Тогда функция для нахождения всех свободных переменных будет выглядеть следующим образом.

Code
let rec fv expr =      
     match expr with
       Var a -> [a]
      |App (p, q) -> unite (fv p) (fv q)
      |Abs (x, r) -> filter (fun z -> (z <> x)) (fv r);;

Функция для нахождения всех связанных переменных чуть посложнее.

Code
let bound expr =
    let rec bound expr =
     match expr with
       Var x -> (false, [x])
      |App (p, q) -> let ((rp, vp), (rq, vq)) = (bound p, bound q) in (rp || rq, unite vp vq)    
      |Abs (x, r) -> (true, List.filter ((<>) x) (snd r)) in
    let (rx, vx) = bound expr in if rx then vx else [];;

(писалось без компилятора, правильности не гарантирую)

И, наконец, альфа-эквивалентность. Я думаю, здесь проще не приводить определения, а сразу дать код, ибо он практически дословно повторяет это самое определение.

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) );;

let rec (=@) a b =
    match (a, b) with
      (Var x, Var y) -> x = y
     |(App (p1, q1), App (p2, q2)) -> (p1 =@ p2) && (q1 =@ q2)
     |(Abs (x, p1), Abs (y, p2)) -> (replace p1 x (Var y)) =@ p2
     |_ -> false;;
 
Форум » Билеты к экзаменам » Программирование » 01 Синтаксис лямбда-выражений
Страница 1 из 11
Поиск:

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