Обсуждение:Лямбда-исчисление

Обсуждение

Правило подстановки -- центральное в λ-исчислении, оно никак не обсуждается. Упущено и отношение конвертируемости.--VEW 16:25, 23 марта 2008 (UTC)

Это верно. Статья не полна. Возьметесь дописать? Хацкер 00:11, 26 марта 2008 (UTC)

Постараюсь. --VEW 16:22, 26 марта 2008 (UTC)

Это соображение в общем виде записывается как

$(\lambda x.t)\ a=t[a:=x],$

и носит название β-редукция. -- возможно ошибка и правильно так:

$(\lambda x.t)\ a=t[x:=a],$

-- ВВ 195.60.245.246 09:53, 11 ноября 2008 (UTC)

совершенно верно. спасибо. Хацкер 12:24, 11 ноября 2008 (UTC)

Удаление абзаца

Не мог не удалить следующий абзац из секции "η-преобразование"

Надо отметить, что если рассматривать лямбда-термы не как функции, а именно как алгоритмы, то данное преобразование не всегда уместно: существуют случаи, когда вычисление $\lambda x.f\ x$ завершается, а вычисление $f$ не завершается.

Это высказывание противоречит теореме Черча-Россера. Согласно теореме Черча-Россера, никогда не поздно вернуться к нормализованной стратегии редукции лямбда-выражений.

Теорема Черча-Россера[1]

Пусть E1 и E2 суть ламбда-выражения, причем справедливо соотношение: E1 = E2.

Тогда существует ламбда-выражение E такое, что выполнены следующие условия: во-первых, E1 = E, и, во-вторых, E2 = E.

Заметим, что символ "=" в формулировке теоремы понимается в смысле отношения конвертируемости.

alanubi 19:56, 8 августа 2010 (UTC)

Язык статьи

Нельзя ли переписать статью? Для не-специалистов понятно очень мало, хотя тема не такая уж и сложная. 213.206.55.129 20:49, 3 сентября 2010 (UTC)

что такое функциональная аппликация и функциональная абстракция - сделайте ссылки какие-нибудь...FeelUs 23:48, 27 января 2011 (UTC)