Что рассказать на обзорной лекции по комбинаторной логике?

[_Ivana]

Спросили на днях, могу ли выступить (в формате онлайн-вэбинара) с такой темой Аудитория - начинающие и продолжающие программисты, интересующиеся "всяким таким". Спецов-математиков, придирающихся к каждой букве определений и доказательств, надеюсь, не будет. Хотя это и не повод нести пургу, конечно
Собственно, ситуация немного осложняется тем, что мои познания в сабже почти отсутствуют. Но и глубокого погружения с разбором доказательств не требуется. Я конечно почитаю про различные комбинаторные базисы, скажу про лыжи SKI, про выражение в них любого замкнутого лямбда-терма и даже имя Моисея Шейнфинкеля упомяну. Но остается вопрос - что показать простого и понятного на пальцах - например, по лямбда-исчислению я бы показал на примерах различие нормальной и аппликативной редукционных стратегий с возможным расхождением и выводами насчет практического применения. А про сабж что можно красивого показать, в идеале с выводами для практических приложений теории?

[arseniiv]

Присоединюсь, интересный вопрос. Люблю темы FP, но совершенно не слежу, так что не знаю, есть ли что-то интересное кроме тьюринг-полноты и детальки о том, чему соответствуют комбинаторы по Карри—Говарду (импликативному фрагменту интуиционистской логики — содержащему не больше, чем нужно для теоремы о дедукции), но какой от них толк самих по себе, не представляю.

_Ivana в сообщении #1355689 писал(а):

например, по лямбда-исчислению я бы показал на примерах различие нормальной и аппликативной редукционных стратегий с возможным расхождением и выводами насчет практического применения

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

Быстрая проверка: определим $YF\to F(YF)$, тогда при стратегии call by value при вычислении $YF$ не остановимся, а при нормальной или, например, call by need, остановимся, если $F$ не редуцируется. Значит, не эквивалентны.

-- Чт ноя 22, 2018 00:36:25 --

Вообще в текстах именно про комбинаторное исчисление (а не про лямбда-исчисление) обычно рассказывают, как на нём можно достаточно сносно выразить разные виды данных (пары, натуральные числа такие и сякие, логические значения). Самостоятельной пользы от этого нет, хотя, видимо, возможность такого выражения интереснее просто тьюринг-полноты (или нет — может, во всяком тьюринг-полном формализме можно найти соответствующие трюки). Можно запутать людей загадочным «логическим» термом $Y\mathsf{not}$ (привет парадоксу лжеца).

Хотя к сожалению кодирование данных (и разные способы) более прозрачно на языке лямбда-исчисления. Пока мы вынуждены выражать все комбинаторы через какой-то небольшой базис, это очень непрозрачно; если не вынуждать себя, куда ни шло.

-- Чт ноя 22, 2018 00:49:48 --

Вру про Карри—Говарда, для того исчисление комбинаторов должно быть не абы каким, а типизированным, то есть аппликации можно составлять и комбинаторы рассматривать не произвольные.

-- Чт ноя 22, 2018 00:51:15 --

В общем, лучше свериться с литературой, если захочется эту деталь рассказывать.

[Munin]

_Ivana в сообщении #1355689 писал(а):

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

В такой ситуации однозначный ответ "нет, не могу выступить".

[_Ivana]

Munin в сообщении #1355902 писал(а):

В такой ситуации

лучше молчать, если нечего сказать по теме, чем флудить.

arseniiv Спасибо. Запилил приводятор любых замкнутых лямбда-термов к лыжному базису, а также визуализатор и эвалюатор последнего. Думаю прямо онлайн накидывать разные примеры - факториалы и прочее в лямбдах, демонстрировать приведение их к лыжному виду и эвалюацию. Надеюсь, это будет наглядно и интересно.

[george66]

Сильно подозреваю, что Шейнфинкель - фигура мифическая. Недавно читал англоязычный обзор по истории лямбда-исчисления, там так прямо и написано "родился в Днепропетровске в 18.. году" (не помню точную дату). И хорошо, что не в Ленинграде (Днепропетровск назван в честь большевика Петровского). Просто главная наука уже не физика, а генетика и компьютер-сайнс, поэтому Эйнштейн в качестве величайшего гения всех времён больше не годится.