Observations

Может быть; мне важен пока принцип только.

From:

anhinga-anhinga.livejournal.com

Собственно, если бы не появившаяся в какой-то момент мода включать полиномиальную эквивалентность по run-time complexity в тезис Чёрча, то было бы совсем не важно...

Но когда люди стали это делать (все широко используемые системы, вроде, полиномиально эквивалентны), то некоторое количество систем перестало быть first-class citizens...

И есть ощущение, что там что-то фундаментальное в этом месте (я сам не знаю)...

From:

А, вот откуда это берется, новая интерпретация тезиса Черча. Похоже на ультраинтуиционизм.

From:

Я немного не понял - алгоритм abstraction elimination дан Тёрнером в 79 году (и, судя по названию статьи, не первый такой, просто тот, который сейчас все знают). Все модели лямбда-исчисления разные, но эквивалентные. (И интересны только алгебраистам - но это наглое оценочное суждение, конечно! Хотя покажите мне кого-нибудь, кто читал все это в Хиндли или Барендрегте, не вставив спички в глаза.) А в чем цимес, цимес-то в чем? Где новизна, и почему бы не обратиться вместо этого к первоисточникам, которым не требовался сопряженный функтор дабы дойти до нужника?

From:

nponeccop.livejournal.com

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

Можно сделать просто формальную систему c 3 константами a, b, c и одним функциональным символом F:

F(a, a) = a
F(a, b) = a
F(a, c) = a
F(b, a) = b
F(b, b) = с
...

Это совсем без привлечения функторов, но не очень понятно.

Можно объяснять в терминах школьной арифметики

Можно приплести общие понятия группы и функции из теории множеств.

И так далее.

Ещё есть чисто техническая проблема модульности. Часто для работы нужно несколько разных теорий, и удобно, если все они описаны в терминах какой-то одной большой теории, вроде теории множеств или ТК. "Тонкие" теории вроде описанной формальной системы с 4 символами плохо склеиваются друг с другом.

Edited Date: 2015-05-19 02:12 pm (UTC)

From:

Да, дело-то именно в том, к какому нужнику мы идем. И, stretching the metaphor, лучше, по-моему, индивидуальный нужник в каждом огороде, чем один трехэтажный нужник сияющего мрамора на деревню, до которого от моей халупы четыре версты продираться по полям, поросшими дикими функторами.

То есть, о чем я говорю. Есть модель комбинаторной логики, лично мне она неинтересна по призванию, но может быть интересна другим людям, что само по себе весьма прельстиво. Но зачем *в этой модели* доказывать давно известные факты этой самой комбинаторной логики?! Если показать, что наша конструкция - это именно модель КЛ, то все факты КЛ в ней верны автоматически, из замшелых манускриптов. То есть, после Definition 1 должно идти не Functional Completeness, а доказательство того, что TCA моделирует КЛ и т. д., откуда все остальное вытекает само собою. Модульность же!

И вот именно этого я и не понимаю. Опять-таки, то что я не понимаю, какой тут профит, не значит, что его нет, - именно поэтому я и задал вопрос выше.

From:

Мне кажется, если вдруг КЛ вытекает из сопряженных функторов, то это дает много разных чудес, с кванторами, скажем.

From:

Дан объект D. Есть функтор умножения на D (_xD) и функтор возведения в степень D (_^D). Если D изоморфно D^D, то эти функторы коммутируют! Выведите из этого много разных чудес немедленно.

From:

В Вашей книжке эти чудеса описаны?

From:

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

From:

Но функторы хотя бы честно коммутируют?
Я не спец по фактам про бестиповую лямбду, интересно.

From:

(AxD)^D=(A^D)x(D^D)=(A^D)xD
Честно коммутируют, но никаких особых чудес из этого, кажется, не получается. Это скорее пример, что при желании сопряжённый функтор можно найти везде.

From:

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

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

From:

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

From:

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

From:

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

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

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

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

From:

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

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

From:

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

From:

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

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

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

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

From:

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 год.

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

From:

Ok. Спасибо.

From:

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

From:

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

From:

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

From:

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

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

From: