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

[juan_gandhi]

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

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

Comments

[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. Спасибо.