Вокруг "Цитатника"

[Munin]

Ага, потому что он отношение, а не бинарная операция :-(

arseniiv, а вы-то почему до сих пор не пользуетесь Сюткиным? Уж кто-кто...

[arseniiv]

Я пользовался The comprehensive LaTeX symbol list — это да. Вообще если бы я чаще что-то латехом писал — а так я только тут это делаю в основном, и по чайной ложке.

-- Вт июн 25, 2019 03:45:29 --

Ещё я пользовался Detexify несколько раз когда-то.

[Munin]

Витаете, небось, в своих высоких алгебраических облаках... даже на форум спуститься некогда, одарить смертных мудростью Карри-Говарда...

[Pphantom]

Munin в сообщении #1401326 писал(а):

Насколько я помню, SI как международный стандарт действует автоматически как ГОСТ, и даже имеет приоритет перед национальными.

Только всякие надзорные органы это обычно не интересует.

[Anton_Peplov]

Munin в сообщении #1401465 писал(а):

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

Мне просто понравился обыгрыш "вешать топор" в выражении "повисает в воздухе". Про давность шутки не знал.

[arseniiv]

(Облака)

Munin в сообщении #1401348 писал(а):

Витаете, небось, в своих высоких алгебраических облаках... даже на форум спуститься некогда, одарить смертных мудростью Карри-Говарда...

Ну тут как — вроде кто знает, тот уже и так знает — по крайней мере почему-то ничего не спрашивает — а кто не знает, тот начинает спрашивать «а что у вас означают вот эти значки, а вот эти буковки», и тут проще кинуть книжкой типа TaPL Пирса. А витаю я совсем не в высоких алгебраических облаках, а обычных облаках Мирских—Заботных.

[Munin]

Anton_Peplov в сообщении #1401487 писал(а):

Мне просто понравился обыгрыш "вешать топор" в выражении "повисает в воздухе".

А, это да, это моё :-)

arseniiv в сообщении #1401488 писал(а):

по крайней мере почему-то ничего не спрашивает

Ещё бы! Тут чтобы только понять, что надо спрашивать, надо изрядно уже проникнуться! Даже чтобы понять, что вообще об этом надо что-то спрашивать!

Вы бы несли потихоньку просветительскую миссию. Создавали бы темы. Вдруг люди заинтересуются :-)

arseniiv в сообщении #1401488 писал(а):

...и тут проще кинуть книжкой типа TaPL Пирса.

Но можно ведь и рассказать! А то книжка - вещь тяжёлая. (И никто, кроме вас, даже названия её не знает...)

[arseniiv]

Знает, я упоминал полное в каком-то месте на форуме (вместе с этим сокращением, так что ищется), но вообще это Types and programming languages. У неё ещё есть продолжение — Advanced topics in types and programming languages.

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

В первом у нас есть базовые комбинаторы $\mathsf{K, S}$ с типами $\mathsf K\colon\alpha\to\beta\to\alpha$ и $\mathsf S\colon(\alpha\to\beta\to\gamma)\to(\alpha\to\beta)\to\alpha\to\gamma$, и можно получить из комбинаторов $A\colon\alpha$ и $B\colon\alpha\to\beta$ комбинатор $(BA)\colon\beta$. (Стрелку $\to$ я считаю здесь везде правоассоциативной, что и естественно.)

Во втором у нас есть аксиомы $a\to b\to a$ и $(a\to b)\to(a\to b\to c)\to a\to c$ и есть правило вывода Modus ponens: $\dfrac{a,\quad a\to b}b$.

Видно, что $\mathsf{K, S}$ и аксиомы друг другу соответствуют (почти: я записал вторую аксиому в более традиционном для неё виде, но в ней можно поменять порядок «аргументов» и иметь $(a\to b\to c)\to(a\to b)\to a\to c$), а аппликация комбинаторов, позволяющая строить новые, соответствует MP, позволяющему получать новые теоремы. Конечно, тут нам везёт, что сейчас это соответствие такое буквальное, ведь есть эквивалентные аксиоматизации второй логики и эквивалентные базисы в первом исчислении, и можно выбрать их так, что соответствие будет не таким наглядным. И даже MP может быть иногда заменён чем-то ещё, хотя для импликативного фрагмента такое выглядело бы неестественным.

Теперь должны стать понятнее слова «термы-типы соответствуют высказываниям, термы-значения соответствуют выводам», хотя тут ещё мало что можно увидеть.

Дальше всё просто наращивается. Например, можно перейти к просто типизированному λ-исчислению с одного края и к натуральной дедукции (опять же интуиционистской и ограниченной формулами с одной импликацией) с другого: абстракция будет соответствовать превращению вывода из гипотезы в безусловный вывод импликации (в гильбертовском исчислении это метатеорема, а не правило вывода — оно недостаточно выразительно, чтобы сделать её «настоящим» правилом). Правило типирования λ-абстракции такое: $\dfrac{\Gamma, x\colon\beta\vdash A\colon\alpha}{\Gamma\vdash(\lambda x.A)\colon\beta\to\alpha}$ — и его можно прочитать как операцию над натуральным выводом: если у нас в нём есть подвывод из гипотезы $\beta$, помеченной маркером $x$ некоторого $\alpha$ (и весь этот подвывод мы могли бы назвать выражением $A$), мы можем дальше вывести $\beta\to\alpha$ и разрядить гипотезу $x$, то есть её больше нигде нельзя использовать (и такой вывод обозначим как $\lambda x.A$, и в нём $x$ уже не встречается свободно, он «инкапсулирован»). $\Gamma$ означает все прочие ещё не разряженные гипотезы — множество каких-то других предположений вида $v\colon\tau$ — они в новом выводе остаются неразряженными.

[Munin]

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

В общем, предлагаю вам всё это скопировать в отдельную новую тему, и в конце сказать "есть вопросы?". Я уверен, что будут :-)

[arseniiv]

Munin в сообщении #1401506 писал(а):

И для новичков удобней было бы стрелку считать не правоассоциативной, а всюду расставлять скобочки.

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

Я подумаю, но в текущем виде это выглядит как-то оторванно. Да, в идеале надо все исчисления описывать целиком, и это как раз проще сделать, ткнув в книжку. Может, надо вообще начинать с идей и получать исчисления прямой реализацией этих идей. И это может быть естественнее всего в категорном воплощении, но я в нём плаваю.

[Munin]

А можно эти формулы как-то декаррировать осмысленно?

[arseniiv]

Munin
Ловите страшный пост: «Введение в изоморфизм Карри—Говарда для кофейников»

-- Ср июн 26, 2019 03:18:29 --

Munin в сообщении #1401524 писал(а):

А можно эти формулы как-то декаррировать осмысленно?

Тут надо иметь в виду, что сами типы, конечно, не обязательно показательны, и нагляднее поведение самих комбинаторов: $Kxy = x,\; Sxyz = (xz)(yz)$, то есть например декаррированный $K$ это просто $(x, y)\mapsto x$, левая проекция из пары, а декаррированный $S$ не особо лучше исходного. Однако у этой парочки есть смысл в переписывании произвольного комбинатора, записанного как λ-терм, в запись из K и S без лямбд. И эта процедура соотносится с доказательством леммы о дедукции. Да, надо будет это тоже включить в ту тему.

[Munin]

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

[arseniiv]

Ну, тема никуда не денется (надеюсь), а мне есть чем заняться.

[fred1996]

arseniiv в сообщении #1401560 писал(а):

Ну, тема никуда не денется (надеюсь), а мне есть чем заняться.

(Оффтоп)

В масштабах Munina долгая пауза - это примерно пара часов.