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 год.
В любом случае, статья Тёрнера очень короткая, и никаких доказательств в ней нет -- зато они есть в учебнике Хиндли, в девятой главе, которая вся об этом! но я туда за ссылками больше сегодня не пойду, эта книга высасывает душу.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2015-05-20 08:07 pm (UTC)> Но в любом случае есть смысл приводить это доказательство в вики, как основной факт об обсуждаемой структуре, не требуя прочесть предварительно 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 год.
В любом случае, статья Тёрнера очень короткая, и никаких доказательств в ней нет -- зато они есть в учебнике Хиндли, в девятой главе, которая вся об этом! но я туда за ссылками больше сегодня не пойду, эта книга высасывает душу.