Связанные, связывающие и свободные вхождения переменных.
- в абстракцию \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;;