Е

Иллюстрация ромбического свойства на примере

сли к терму нельзя применить бета-редукцию, то говорят, что он находится в нормальной форме. Например, (x.M) N – не в нормальной форме, а x или x.x x – в нормальной форме. Некоторые термы нельзя свести к нормальной форме. В качестве примера можно привести терм (x.x x) (x.x x) . Другие выражения в зависимости от стратегии вычисления могут давать или не давать результата, например, (y.0)(( x.x x)( x.x x)). Существует два основных метода получения нормальной формы - вызов по значению, когда сначала производится подстановка в самых внутренних редексах, и вызов по необходимости, когда сначала производится подстановка в самом внешнем редексе (слева). Если нормальная форма достижима, то она всегда может быть получена стратегией вызова по необходимости, однако вызов по значению обычно требует меньше редукций.

Прикладные лямбда-исчисления

Прикладное лямбда-исчисление отличается от чистого тем, что в него вводится набор констант c, характеризующий данную предметную область. В этом случае грамматика лямбда-выражения такова:

M = c | x | (M₁ M₂) | (x.M)

Константы иногда представляют в постфиксной форме, например, X’ = ’(X) или A + B = (A +) B = ((+ A) B). Здесь следует понимать, что + является константой прикладного лямбда-исчисления.

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

Рассмотрим пример прикладного лямбда-исчисления. Определим следующий набор констант: true false if not and or eq 0 next plus. Определим правила сигма-редукции(предметные правила).

Правило	Комментарий
not true  false	Данные правила частично являются стандартными правилами математической логики, частично – арифметики, при соблюдении следующих условий. Под not следует понимать инверсию, or – дизъюнкцию, and – конъюнкцию. True и false соответствуют логическим единице и нулю. Оператор If может быть представлен более сложным образом, например в виде (or (and x y (not a)) (and y (not x) (not a)) (and a x (not y)) ( and a x y))3. eq является выражением эквивалентности, а 0 – числом 0. plus представляет собой сложение, next - инкремент
not false  true
or false x  x
or x false  x
or x true  true
or true x  true
if true x y  x
if false x y  y
and false x  false
and x false  false
and x true  x
and true x  x
eq true true  true
eq false false  true
eq true false  false
eq false true  false
eq 0 0  true
eq (next x) 0  false
eq 0 (next x) false
eq (next x) (next y) eq x y
plus 0 x  x
plus (next x) y  next (plus x y)

Большая часть данных правил соответствует обычной математической логике. В свете этого можно следующий пример, записанный в терминах языка Паскаль, вычислить с помощью лямбда-исчисления:

if 1+1=2 then return A else return B

if (eq (plus (next 0) (next 0)) (next (next 0))) A B =>

if (eq (next (plus 0 (next 0)) (next (next 0))) A B =>

if (eq (next (next 0)) (next (next 0))) A B=>

if (eq (next 0) (next 0)) A B =>

if (eq 0 0) A B=>

if true A B =>

A