2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему
 
 Что рассказать на обзорной лекции по комбинаторной логике?
Сообщение21.11.2018, 18:27 


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

 Профиль  
                  
 
 Re: Что рассказать на обзорной лекции по комбинаторной логике?
Сообщение21.11.2018, 22:21 
Заслуженный участник


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

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

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

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

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

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

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

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

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

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

 Профиль  
                  
 
 Re: Что рассказать на обзорной лекции по комбинаторной логике?
Сообщение22.11.2018, 15:31 
Заслуженный участник
Аватара пользователя


30/01/06
72407
_Ivana в сообщении #1355689 писал(а):
Спросили на днях, могу ли выступить (в формате онлайн-вэбинара) с такой темой...
Собственно, ситуация немного осложняется тем, что мои познания в сабже почти отсутствуют.

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

 Профиль  
                  
 
 Re: Что рассказать на обзорной лекции по комбинаторной логике?
Сообщение22.11.2018, 16:05 


05/09/12
2587
Munin в сообщении #1355902 писал(а):
В такой ситуации
лучше молчать, если нечего сказать по теме, чем флудить.

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

 Профиль  
                  
 
 Re: Что рассказать на обзорной лекции по комбинаторной логике?
Сообщение23.11.2018, 02:28 
Заслуженный участник


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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 5 ] 

Модераторы: Модераторы, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group