затягивает чтение...

[juan_gandhi]

http://ncatlab.org/nlab/show/partial+combinatory+algebra

Так из нефиг делать лямбды лепятся в ССС и в топосе...

Comments

[zeit-raffer.livejournal.com]

> лучше, по-моему, индивидуальный нужник в каждом огороде,
> чем один трехэтажный нужник сияющего мрамора

Продолжая метафору, в городах почему-то предпочитают централизованную канализацию. Индивидуальные нужники (как "в огородах") в многоквартирных домах не справляются. Вот ТК или ТМ - это такие централизованные системы минимизации энтропии, более или менее технологичные.

[pbl.livejournal.com]

И все-таки это, по-моему, совершенно не отвечает на вопрос: "Зачем показывать старый и хорошо известный результат на аппарате ТК, вместо того чтобы доказать, что все наши огородные результаты имеют место и в этой модели?"

[juan-gandhi.livejournal.com]

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

[pbl.livejournal.com]

> Ну, во-первых, категорщику этот результат совершенно был неизвестен

Вот это многое объясняет, на самом деле. Я смотрю на это с точки зрения человека, который немножко понимает в КЛ и лямбда-исчислении, но ничего не понимает в теоркате. С противоположной перспективы все по-другому выглядит, конечно, что мне и трудно представить.

> для кого-то это "контейнер для данных"

Ну это совсем нелестное сравнение для нас, сермяжных погромистов, потому что это представление неконсистентно же. Настоящие сермяжные погромисты представляют монады как композицию эффектов, даже те которые как бы "контейнеры".

[zeit-raffer.livejournal.com]

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

Во-вторых, я не настолько спец в КЛ, чтобы определить, повторяют ли они её результаты. Насколько я понимаю, в КЛ это утверждение доказывается для частного случая A={лямбда-выражения} (синтаксическая модель) и без дополнительных оговорок перенести его на любую модель нельзя (хотя можно проверить, что практически то же доказательство работает для любой модели, чем на этой странице и занимаются).

[pbl.livejournal.com]

См. J. Roger Hindley , Jonathan P. Seldin, Lambda-Calculus and Combinators: An Introduction -- 9, 14, 15, 16, в частности 15.12, 15.30 и оттуда далее.

[zeit-raffer.livejournal.com]

Theorem 15.12 Every λ-model satisfies all the provable equations of the formal theory λβ.

Вопрос в том, можно ли выразить свойство Functional completeness в виде простого равенства, чтобы это было применимо. Там же еще потребуется префикс "для любой формулы в лямбде существует формула без лямбды", вот он, подозреваю, не моделируется.

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

Вам не трудно сослаться еще и на "дан Тёрнером в 79 году"? Хочу понять, он доказывал для самой лямбды или для моделей?

[pbl.livejournal.com]

15.12 (с corollaries) интересно для обсуждения и бэкграунда, но ключевое там 15.30, по-моему -- "every extensional combinatory algebra [...] can be made into a λ-model." По-моему, это перспективнее, чем воспроизводить отдельные результаты в КТ.

> Но в любом случае есть смысл приводить это доказательство в вики, как основной факт об обсуждаемой структуре, не требуя прочесть предварительно 235 страниц монографии.

Granted. Контекст несколько меняет дело. Хотя "основной факт," опять-таки, зависит от точки зрения -- этот факт довольно частный, вообще говоря. Кроме того, мне мстится здесь некоторое лукавство. Ну вот зайдет категорно невинный программист на эту статью в вики, что он обо всем этом подумает?! Я как категорно невинный программист могу предположить -- что тут надобно прочитать какую-нибудь (несуществующую в природе!) доступную монографию о КТ, чтобы разобраться, что пишут все эти блистательные люди со своими топосами об искоренении абстракции. Ну хотя бы ссылку можно было поставить на prior art?

> Вам не трудно сослаться...

Конечно -- http://www.jstor.org/stable/2273733?seq=1#page_scan_tab_contents

Но я безбожно вру, как выяснилось. Я увидел знакомый алгоритм после слов "Perhaps the simplest algorithm for bracket abstraction is as follows," и решил что это и есть вклад Тёрнера. При более внимательном чтении по диагонали выяснилось, что, как минимум, "Curry [1] gives an improved version..." (с B и C) -- это:

[1] H. B. CURRY and R. FEYS, Combinatory logic, vol. 1, North-Holland, Amsterdam, 1958.

Дальше я уже не пошел по ссылкам.

Кроме того там упоминается, что "This very significant result was first discovered by Schoenfinkel [3]," чего я не знал о его комбинаторном базисе, это вообще 24 год.

В любом случае, статья Тёрнера очень короткая, и никаких доказательств в ней нет -- зато они есть в учебнике Хиндли, в девятой главе, которая вся об этом! но я туда за ссылками больше сегодня не пойду, эта книга высасывает душу.

[zeit-raffer.livejournal.com]

Ok. Спасибо.

[juan-gandhi.livejournal.com]

Вот еще фактор. Ваша лямбда где-то моделируется, где-то нет. В теории множеств привыкли; а если у нас логика не булева? А если время добавить? И т.д.

[pbl.livejournal.com]

Я не готов сам это доказывать, но нутро упорно мне подсказывает, что структуры-то из вышеприведенной статьи и есть модели КЛ и лямбда-исчисления. Я ж потому и буяню здесь, что вроде как да, и терминология знакомая!.. а доказательство отсутствует (или упоминание, что таки нет). Или вообще хоть какая-нибудь привязка. Это ж не так, что существует одна (или дюжина) каноническая модель. Их бесконечно много, и в любой верны все результаты, которые на свойства модели вообще никак не опираются.

[juan-gandhi.livejournal.com]

Да, конечно. Но так вот с ходу поверить, что в небулевом топосе это все столь же справедливо, это ж надо все еще раз повторить и убедиться.

[66george.livejournal.com]

От изобретения моделей Скотта была одна немедленная польза: решили старый вопрос "какие лямда-термы следует считать зацикленными". В моделях есть наименьший элемент, ему равны термы без головной нормальной формы. Посмотрев на модели, Уодсворт придумал головную нормальную форму.

У меня к программистам такие же претензии "Почему не написать человеческим языком?" Ищу понятный текст вроде "Как взломать vbulletin", нахожу или дикий жаргон (типа "засунь парсер в обфускатор") или комиксы с поросятами. Связного изложения, от простого к сложному, без жаргона почти не найдёшь. Но это общая проблема, не только у программистов.

[pbl.livejournal.com]

Именно, общая проблема. У меня те же самые претензии к погромистам.