Связанная переменная

Материал из свободной русской энциклопедии «Традиция»
Перейти к: навигация, поиск

Связанная переменная (связанный идентификатор) — в λ-исчислении переменная \(v\), входящая в некоторый λ-терм \(M\) и удовлетворяющая одному из следующих условий:

  1. \(M = \lambda v'.M'\), и \(v = v'\);
  2. \(M = (M_1 M_2)\), и \(v\) связана в \(M_1\) или \(M_2\) (то есть один и тот же идентификатор может быть как свободен, так и связан в λ-терме);
  3. \(M = (M')\), и \(v\) связана в \(M'\).

Множество переменных \(v\), связанных в терме \(M\), обозначается как \(BV(M)\) (от англ. bounded variable — связанная переменная).

См. также[править]