[CS][λ] Интересные развития исчисления.

Кастование что, заработало в темах? Последний раз, как видел, работало только в комментариях.

блин, подумал что трэд про халфу и контру

> Кастование что, заработало в темах? Последний раз, как видел, работало только в комментариях.

ХЗ. На всякий пожарный.

Например добавляющие парочку каких-либо правил, или вводящих другие сущности.

Если практически, то, например, `case' у GHC — когда в языке помимо базового исчисления появляются индуктивные ADTs, то нужно вводить такую специальную форму для поддержки деконструкции (паттерн-матчинг) этих данных. Или `cast' для GADTs у того же GHC. Или `let/letrec' как только в λ-исчислении появляются (даже простые) типы. Ну и вообще — любая захардкоженная специальная форма (т.е. нечто, что нельзя сделать с помощью обычных функций, что не укладывается в их стратегию редукций) может потребовать расширения core-языка; поэтому у scheme, haskell и других языков имеющих к λ-исчислению какое-то отношение core язык > обычного λ-исчисления.

Кроме типизированных вариантов.

А они все типизированные - безтиповое λ-исчисление это просто вырожденая форма всего с одним типом. А обогащение языка типов сказывается и на языке термов — там появляются новые вещи помимо переменных, абстракции и аппликации (например, абстракции и аппликации для типов, произведения и суммы с проекциями и инъекциями).

Кроме того, что почитать по семантике языков программирования?

Теорию категорий :) В частности, любой формальный язык так или иначе имеет «типы» (высказывания в логике, обычные типы в языках программирования), «термы» (доказательства в логике и синтаксически правильные конструкции в языках программирования) и «редукции» (правила вывода и конкретные вычисления, соответсвенно). Категорно эти три вещи суть объекты, стрелки и 2-стрелки. На уровне объектов у нас типы, на уровне стрелок — синтаксис, а на уровне 2-стрелок — семантика. Ну и становится понятно, что нетипизированных языков, в буквальном смысле, не бывает — не может быть категории без объектов. Бывают только языки с бедными типами.

Что можно почитать — Introduction to Categories and Categorical Logic, там сначала теория категорий разжёвывается, а потом строится логика натуральных дедукций и просто-типизированное λ-исчисление как CCC (и доказывается их изоморфизм), и ещё линейные версии логики и λ-исчисления как SMCC (тоже изоморфные). Примерно на ту же тему, но ещё с физикой и топологией есть Physics, Topology, Logic and Computation: A Rosetta Stone.

Небольшой пример с использованием haskell-я — безтиповое λ-исчисление.

> {-# LANGUAGE TypeOperators, MultiParamTypeClasses, FunctionalDependencies
>   , FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes
>   #-}

Сначала будем считать, что у нас есть единственный объект (т.е. тип) Dyn.

В качестве переменных используем мета переменные в хаскельных типах (т.е. variable swaping делать не нужно). Для переменных справедливо:

  Var ∋ x, y, z, ...

  
  -----------
  Γ ⊢ x : Dyn

Термы, то есть стрелки:

  Term ∋ t, u ::= x | t u | λ x . t


  -----------------
  Γ ⊢ λ x . t : Dyn


  -------------
  Γ ⊢ t u : Dyn

> data L x
> data f :. x
> infixl 2 :.

Все остальные синтаксически правильные термы — композиции этих стрелок.

Может быть не совсем понятно, что есть Dyn, можно нарисовать две такие диаграммы:

  1 --|z|--> N <--|s|-- N

  N --|var|--> Term <--|λ|-- Term
                ^
                |
              |app|
                |
           Term × Term

т.е. все объекты (типы) которые нужны — начальный объект (bottom type), счётный тип (изоморфный натуральным числам — для представления мета-переменных) и тип Term. Т.е. в нетипизированном языке любая конструкция просто типизируется как Term (он же expression, он же AST). Ну и пара термов Term × Term (произведения в категории при этом и не обязательны).

Редукции, то есть 2-стрелки:

> class A l a b | l a -> b

Это элементарные редукции, все остальные редукции — 2-композиции 2-стрелок, а полная (терминальная) редукция определяется как:

> infixr 1 :=>
> class a :=> b | a -> b

> instance                                       (:=>) (L x) (L x)
> instance (y :=> y', A (L x) y' r)           => (:=>) ((L x) :. y) r
> instance ((x :. y) :=> r', (r' :. z) :=> r) => (:=>) (x :. y :. z) r

И всё. Дальше, определение «констант» в языке это определение стрелок из терминального объекта в единственный тип Dyn (ну или Term), к примеру:

> data T
> data F

  1 --|t|--> Term

  1 --|f|--> Term

«Константы» это самовычислимые объекты, поэтому элементарные 2-стрелки (редукции) это просто:

> instance (:=>) T T
> instance (:=>) F F

  |t| ==|eval t|==> |f|

  |f| ==|eval f|==> |t|

Что касается определения функций, то их мы сначала задаём на синтаксическом уровне как стрелки:

> data Not
> data And

  1 --|not|--> Term

  1 --|and|--> Term

и на семантическом уровне как элементарные 2-стрелки:

> instance A (L Not) T F
> instance A (L Not) F T

> instance A (L And)      x (L (And,x))
> instance A (L (And, T)) a a
> instance A (L (And, F)) a F

В общем, определения (в том числе рекурсивных) функций это системы элементарных 2-стрелок, а полные редукции, это те или иные 2-композиции. Например:

> type Test x y =
>   -- and (not x) (not y)
>   ((L And :. (L Not :. x) :. (L Not :. y)) :=> r) 
>   => r

> __ = __

> test = __ :: Test F T

Вот примерно так в хаскеле можно конструировать лямбда исчисление в категорных терминах (во многом благодаря тому что механизм классов типов это, фактически, логическое программирование на типах). Вся это категория довольно простая, можно поставить вопрос о том какой логике изоморфно нетипизированное λ-исчисление — в принципе, никакой. Это логика всего с одним высказыванием и с возможностью повторять это высказывание. По мере того как модельная категория ограничивается новыми свойствами моделируемые языки и логики становятся более мощными — сначала линейными, потом «классическими», а вариант зависимых типов соответствует замкнутым категориям.

произведения в категории при этом и не обязательны

Помарка, таки нужны.

Помарка, таки нужны.

И играют роль лисповых пар :)

а вариант зависимых типов соответствует локальным категориям.

fixed

Ещё вспомнил - quote (как в лиспах). Как 2-стрелка она не определяется, вместо этого нужно расширять правила вывода:

> data Q t

  Term --|quote|--> Term

> instance (:=>) (Q t) t

> type Test' x y =
>   (Q (L And :. (L Not :. x) :. (L Not :. y)) :=> r) 
>   => r

> test' = __ :: Test' T F

  :t test'
  -- > test' :: (L And :. (L Not :. T)) :. (L Not :. F)

т.е. выражение не вычисляется - цитируется.

> Теорию категорий :)

Это в каком месте теоркат связан с семантикой? Семантика у ЯП бывает только одна - операционная. Все остальное - от лукавого.

Семантика у ЯП бывает только одна - операционная.

Операционная, денотационная, деривационная - это всё в ВУЗах проходят. В принципе, это модели использующие классические математические методы - наивную теорию множеств, какую-то логику.

Только это уже давно (мягко говоря) не последнее слово.

Все остальное - от лукавого.

Ну тогда весь последний выпуск «Lecture Notes in Physics» тоже от него? ;)

У треда тэг CS, а CS без теории категорий это вовсе не CS, это частные пляски с прикладной математикой.

Это в каком месте теоркат связан с семантикой?

Где-то в области естественных преобразований и 2-стрелок, как я понимаю.

> Операционная, денотационная, деривационная - это всё в ВУЗах проходят. В принципе, это модели использующие классические математические методы - наивную теорию множеств, какую-то логику. Только это уже давно (мягко говоря) не последнее слово.

Вы о чем? Это же разновидности семантик, а не способов их описания. Какие методы хотите - такие и используйте. Алсо - что это еще за такие «неклассические» методы? Торсионные поля?

У треда тэг CS, а CS без теории категорий это вовсе не CS, это частные пляски с прикладной математикой.

Еще дедушка Маклейн упоминал, что уровень абстракции обратно пропорционален уровню содержания. И завещал быть осторожными - в качестве категории можно рассмотреть все, что угодно, но нужно - лишь очень, очень редкие объекты. Теоркат весьма хорош в логике - потому что в логике как раз полно очень абстрактных объектов, которые не к чему привязать. Из-за изоморфизма Карри-Говарда мы получаем теоретико-категорное описание CS «искаробки», но оно выходит абсолютно безсодержательным, т.к. уровень абстракции в CS на порядок ниже уровня абстракции формальной логики. Удел теорката в CS (и вообще в любой дисциплине, которая не предполагает наличия серьезных абстракций) - переписывние на теоретико-категорный язык уже известных фактов. И практика это подтверждает - ничего нового за все время.

Ну тогда весь последний выпуск «Lecture Notes in Physics» тоже от него? ;)

Я поясню. Семантика ЯП имеет смысл лишь настолько, насколько она проясняет вычислительную модель ЯП. Тогда, на основе этой семантики, мы можем делать эффективные утверждения о свойствах программ, написанных на этом ЯП. Операционная - проясняет (операционная семантика - это и есть вычислительная модель де-факто). А та же денотационная (для которой как раз теоретико-категорное представление оптимально) - нет. Если у вас есть операционая семнатика и некоторая программа, то вы можете исследовать любое, интересное на практике, свойство этой пограммы. Для денотационной семантики такое утверждение уже не будет верным. Фактически - такая семантика вообще не дает нам никакой актуальной информации.

Ну вот вы взяли обычную операционную семантику обычного нетипизированного лямбда-исчисления и перевели на язык теорката (кстати, наличием единственного типа вы нигде не воспользовались, можно было остановиться на типе term, как типе в метаисчислении). Что вы получили? Ничего, ну кроме того, что в классическом варианте изложение составляет полстраницы и практически не требует привлечения сторонней терминологии (как у вас - стрелки, 2-стрелки, композиции, терминальные объекты и произведения...)

> блин, подумал что трэд про халфу и контру

Плюсую.

лорчую, заумался =\

http://bash.org.ru/quote/399197

Это же разновидности семантик, а не способов их описания. Какие методы хотите - такие и используйте.

Ну да, много частных методов, которые всё об одном. А ТК позволяет говорить унифицированно.

Алсо - что это еще за такие «неклассические» методы?

Это про CL / IL (и элементарный / неэлементарный топос).

Вообще, категорные методы имеются ввиду. Без них у нас в логике будет одно, в топологии другое, в CS - ещё какие-то свои конструкции. С другой стороны, категорно можно везде выделить одни и те же (с точность до) структуры. И без этого - не видно ни связи между интуиционистской логикой и лямбда-исчислением, ни возможности ослабить свойства категории до линейных вариантов логик и исчисления, ни возможности определять модель теории топосом (и там вообще может быть _не_ set-based модель). Не говоря уже о более простых вещах - подъязыках как подкатегорий, функторах между языками (в том числе сопряженных) и т.п.

Еще дедушка Маклейн упоминал, что уровень абстракции обратно пропорционален уровню содержания. И завещал быть осторожными

Да ради бога :)

т.к. уровень абстракции в CS на порядок ниже уровня абстракции формальной логики.

Начиная с проникновения (хоть и медленного) дисциплин programs as proofs в программирование (coq, agda, частично haskell) это уже не так.

И практика это подтверждает - ничего нового за все время.

Именно в CS? Видимо да. Пока ТК играет больше описательную роль. Тем не менее, даже чисто библиографически это уже сложившийся раздел CS, так что после ознакомления с «классикой» хорошо бы с ним ознакомиться.

Семантика ЯП имеет смысл лишь настолько, насколько она проясняет вычислительную модель ЯП.

Правильно, категорная семантика имеет в этом смысле ту же ценность, что и операционная или денотационная. Т.е. с её помощью можно дать определение семантики внутренними средствами (2-стрелок), либо внешними (с помощью функтора в другую категорию).

кстати, наличием единственного типа вы нигде не воспользовались, можно было остановиться на типе term, как типе в метаисчислении

Наоборот, он активно используется. В комментариях - в коде на хаскеле, да, это не видно. Но с точки зрения стрелок и 2-стрелок то что объект один имеет решающее значение.

Ну вот вы взяли обычную операционную семантику обычного нетипизированного лямбда-исчисления и перевели на язык теорката ... Что вы получили?

Нет, я не предлагаю «переводить», я предлагаю _сразу_ говорить на языке категорий.

Ничего, ну кроме того, что в классическом варианте изложение составляет полстраницы и практически не требует привлечения сторонней терминологии

Зато оно требует привличения теории множеств. Аксиоматика навроде NBG или ZF это своего рода метематический ассемблер, их можно использовать чтобы формально определить метакатегории, после чего язык категории это уже что-то вроде высокоуровнего языка, пригодного для определения как классических теорий (множеств + логики), так и неклассических.

>блин, подумал что трэд про халфу и контру

+1

http://www.cs.uiowa.edu/~astump/papers/archon.pdf используется Scott Encodings для представление данных, небольшое расширение лямбда исчисления и получается язык в котором можно записать что такое альфа-эфквивалентность термов этого языка.

> что почитать по семантике языков программирования?

ISBN 978-5-93972-757-0

> Ну да, много частных методов, которые всё об одном. А ТК позволяет говорить унифицированно.

Не частных, а теоретико-множественных. Таких же унифицированных, как и методы теорката.

Вообще, категорные методы имеются ввиду. Без них у нас в логике будет одно, в топологии другое, в CS - ещё какие-то свои конструкции.

И с ними так же :)

С другой стороны, категорно можно везде выделить одни и те же (с точность до) структуры.

Как и в теории множеств.

И без этого - не видно ни связи между интуиционистской логикой и лямбда-исчислением, ни возможности ослабить свойства категории до линейных вариантов логик и исчисления, ни возможности определять модель теории топосом (и там вообще может быть _не_ set-based модель).

Можно просто в силу того, что теоркат эквивалентен теории множеств.

Начиная с проникновения (хоть и медленного) дисциплин programs as proofs в программирование (coq, agda, частично haskell) это уже не так.

Наоборот. Как раз тут теоркат не просто не приносит пользы в качестве «давайте переведем все на его язык», но и наносит вред, скрывая за мишурой смысл явлений.

Пока ТК играет больше описательную роль. Тем не менее, даже чисто библиографически это уже сложившийся раздел CS, так что после ознакомления с «классикой» хорошо бы с ним ознакомиться.

Это никак не раздел CS как раз просто потому, что он сугубо описательный. У него нету своей проблематики, нету своего содержания, вы возьмите любую книжку по алгебре - авторы просто берут и применяют теоретико-категорные обозначения там, где это удобно. И теоретико-множественные - там, где это удобно, свободно их мешая и выбирая тот инструмент, который больше подходит. Без всяких вые*онов на тему «ну да вы что, батенька, эта ваша теория множеств - прошлый век». И никто не говорит о «сложившемся разделе». Каждый раз, когда вы собираетесь назвать теоретико-множественную пару (редукцию) 2-стрелкой, задайте себе вопрос - зачем? Если вы не можете на него ответить сразу и четко, значит вы делаете что-то не так. Вы знаете какую-нибудь теорему для 2-стрелок, которая при обратном переводе даст нетривиальное свойство редукций? Нет? Тогда к чему это все? Вы ведь если хотите доказать какое-то равенство для операций над множествами - просто берете ZFC и доказываете, а не рисуете коммутативные диаграммы в нужном топосе, так?

Но с точки зрения стрелок и 2-стрелок то что объект один имеет решающее значение.

Ну вы ведь знаете, что для построения категории нужны только стрелки. А объекты - не нужны. id-стрелку вы в данном случае _можете_ зафиксировать, и эта стрелка свободно выступит у вас в качестве T.

И я

> Нет, я не предлагаю «переводить», я предлагаю _сразу_ говорить на языке категорий.

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

Зато оно требует привличения теории множеств. Аксиоматика навроде NBG или ZF это своего рода метематический ассемблер, их можно использовать чтобы формально определить метакатегории, после чего язык категории это уже что-то вроде высокоуровнего языка, пригодного для определения как классических теорий (множеств + логики), так и неклассических.

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

Правильно, категорная семантика имеет в этом смысле ту же ценность, что и операционная или денотационная. Т.е. с её помощью можно дать определение семантики внутренними средствами (2-стрелок), либо внешними (с помощью функтора в другую категорию).

Вы что-то путаете, категорная/теоретико-множественная и денотационная/операционная - это ортогональные вещи. Вот вы чуть выше дали категорную операционную семантику.

...

Ну, т.е. лично для вас теоретико-множествинный подход вообще и операционные семантики в частности предпочтительнее. Я ведь не против. Просто сам придерживаюсь другой позиции, и вы уже поняли какой :) (_мне_ так удобнее). Так что давайте не будем говорить «семантика у ЯП бывает только одна - операционная. Все остальное - от лукавого» раз уж, по вашему, эти два описания эквивалентны. Ну и не хотелось бы останавливаться в развитии - вот теория множеств вековой выдержки, классическая логика, операционные семантики, и больше ничего не нужно. ТК в этом смысле довольно привлекательный путь развития, как на мой взгляд - по сравнению с ней операционные семантики это просто безрыбье :)

Насчёт эквивалентности:

Можно просто в силу того, что теоркат эквивалентен теории множеств.

Вообще, это не так (ещё раз - неэлементарные топосы, как пример - некоммутативная геометрия).

Без всяких вые*онов на тему «ну да вы что, батенька, эта ваша теория множеств - прошлый век».

В том то и дело, что set-based подход ограничен. Можете называеть это «выебонами», но любая книжка по категорной логике начинает с того, чтобы заставить читателя отвязаться от теории множеств и классической логики.

назвать теоретико-множественную пару (редукцию) 2-стрелкой

А вы распишите свойства для этой пары и для 2-стрелки - это _весьма_ разные вещи, у 2-стрелки гораздо больше структурной информации (они бывают и между композициями обычных стрелок), в отличии от.

Вы знаете какую-нибудь теорему для 2-стрелок, которая при обратном переводе даст нетривиальное свойство редукций?

Например, что-нибудь про coherence и свойство Church–Rosser. В CCC CR работает, а в CMC может и не работать (было бы странно, если бы в квантовой физике, с которой связываются моноидальные категории, был аналог CR).

id-стрелку вы в данном случае _можете_ зафиксировать, и эта стрелка свободно выступит у вас в качестве T.

Как ни назови - объект или id-стрелка, это всё равно одно и то же (чисто аксиоматически удобно писать id : forall {A : Obj} -> A -> A -> Hom A A, это да).

Ясно, то есть ваш план состоит в следующем

Да нет никакого плана. Просто теоретико-стрелочный язык удобен в размышлениях о языках. Особенно это касается сильно-типизированных языков.

И та и та теория будут выступать то ассемблером, то высокоуровневым ЯП в зависимости от контекста.

Тогда осталось объяснить засилье теорката в логике и прочих областях [около]математики в последние десятилетия. Ну не подходит классическая теория множеств на ту роль, которую может играть теоркат.

Вы что-то путаете, категорная/теоретико-множественная и денотационная/операционная - это ортогональные вещи.

Ну да. Я имею ввиду теоретико-множественную форму операционной семантики.

Семантика ЯП имеет смысл лишь настолько, насколько она проясняет вычислительную модель ЯП. Тогда, на основе этой семантики, мы можем делать эффективные утверждения о свойствах программ, написанных на этом ЯП.

Ну щас.

Вот тебе утверждение: для любой функции f с типом forall a. a -> a верно, что f x = x.

При чём тут операционная семантика?

> Вообще, это не так (ещё раз - неэлементарные топосы, как пример - некоммутативная геометрия).

Это так. Вы просто путаете теорию с метатеорией. Когда идет речь о топосах и о функторах в качестве моделей, то теоркат выступает в роли метатеории, так же как ZFC может так же выступать в качестве метатеории в случае классической теории моделей, в этом случае эти теории могут выразить в точности одни и те же вещи.

В том то и дело, что set-based подход ограничен.

Он эквивалентен теоретико-категорному, еще раз. Можно считать, что теория множеств и теоркат - это «железо», аксиоматизация - язык ассемблера. Оба эквивалентные друг другу - и машине Тьюринга :) но архитектура железа разная - разный и ассемблер. Для одних задач - лучше подходит одна архитектура, для других - другая. Теория множеств тут выигрывает за счет того, что для нее придумано множество высокоуровневых языков (фактически каждый раздел математики является таковым), для теорката пока что таких ЯП нет (и неизвестно будет ли, т.к. адекватный формализм для работы с диаграммами как-то плохо представляется), есть только ассемблер (хотя, коненчо, некое развитие в этой области идет).

А вы распишите свойства для этой пары и для 2-стрелки - это _весьма_ разные вещи, у 2-стрелки гораздо больше структурной информации (они бывают и между композициями обычных стрелок), в отличии от.

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

Например, что-нибудь про coherence и свойство Church–Rosser. В CCC CR работает, а в CMC может и не работать (было бы странно, если бы в квантовой физике, с которой связываются моноидальные категории, был аналог CR).

Ну давайте без что-нибудь. Назовите конкретную теорему о 2-стрелках в произвольно взятой категории и переформулируйте ее в рамках терминов предметной области.

Как ни назови - объект или id-стрелка, это всё равно одно и то же

Это не одно и тоже, просто формально два таких подхода эквивалентны. Просто в данном случае вы можете обойтись без типов, когда они не нужны. Зачем множить сущности?

> Да нет никакого плана. Просто теоретико-стрелочный язык удобен в размышлениях о языках. Особенно это касается сильно-типизированных языков.

Еще раз - вы заменили классическое полустраничное определение ламбда-исчисления не вполне внятным переводом на теоретико-категорный язык на несколько страниц, причем изрядно усложнив изложение и навводив кучу лишних сущностей. Причем ничего к оригиналу не добавив (перевод он и есть перевод). В чем проявляется «удобство» в данном случае?

Тогда осталось объяснить засилье теорката в логике и прочих областях [около]математики в последние десятилетия.

Прочих - это каких? Пока что нигде кроме логики да топологии ее и нету (всмысле - применение не выходит за рамки перевода уже известных фактов на новый язык). Да, ее _пытаются_ применять еще где-нибудь - но это свойство любого нового подхода, его будут пытаться применять где можно (с криками о новой серебрянной пуле), а вдруг что-то даст? Что до того факта, что теоркат вообще в принципе может быть где-нибудь успешно применен - тут ничего странного. Есть разные инструменты, которые удобны для решения разных задач. Чтобы забить гвоздь - вы берете молоток, чтобы закрутить гайку - гаечный ключ (взять, я уже упоминал, любой современный учебник по алгебре - и вы увидите как доказательства/определения из теорката и теории множеств спокойно соседствуют друг с другом на одной странице и применяется в каждом конкретном месте тот подход, который более удобен). Но вот теоркат в cs - это как раз нечто из области забивания гвоздей гаечным ключом. Оно, конечно, можно, забьете при желании. Но зачем? Ведь молоток есть. Нет, я согласен, тут ведь сразу, без пробы, и не поймешь, что есть молоток, а что - гаечный ключ, но, мне кажется, уже прошло достаточно времени для «на попробовать».

> Вот тебе утверждение: для любой функции f с типом forall a. a -> a верно, что f x = x.

Ваше утверждение как раз _зависит_ от операционной семантики языка. Если вы имели ввиду обычную типизированную лямбду с полиморфизмом - то из стандартной семантики ваше утверждение можно вывести, да. Для языков с другой семантикой - оно может оказаться неверным. Во-вторых - где вы тут увидели утверждение о свойствах _программы_?.

Ваше утверждение как раз _зависит_ от операционной семантики языка. Если вы имели ввиду обычную типизированную лямбду с полиморфизмом

И где во втором предложении указание на операционную семантику?

Во-вторых - где вы тут увидели утверждение о свойствах _программы_?.

Программа — тоже функция, естественно.

Вы просто путаете теорию с метатеорией.

Я как раз использую ТК как метатеорию. Категории это _модели_ языков. Заданием 2-категории можно задать язык _полностью_. Почему нельзя использовать для этого множества? Потому что заданием множества язык не задаётся (задаётся только множество термов, а все структурные свойства нужно определять отдельно - все эти сторонние построения и есть разные грамматики Хомского или операционные семантики).

Вообще, это всё не наезд на множества, это наезд на использование множеств в качестве моделей (мы ведь про это - про задание моделей ЯП). Множество это объект 0-категории, это «плоская» и невыразительная конструкция. Если использовать объекты n-категории как модели - можно выразить гораздо больше.

В том то и дело, что set-based подход ограничен.

Он эквивалентен теоретико-категорному, еще раз.

Я не знаю что такое «эквивалентен», формально, так что ничего не могу возразить. Но категория Sets это 0-категория. Вообще, чем ниже порядок категории, тем больше «лес» изучаемых структур будет скрываться за «деревьями» частных математических манипуляций. Так, если вернуться к языкам, объекты в Sets (0-категория) это множества, а стрелки это отображения, т.е. языки это множества («язык это подмножество множества всех цепочек над словарём» - получается очень плоско и неконструктивно, структура языка никак не задаётся его множеством), эти множества можно индуктивно конструировать (грамматики Хомского, уже немного конструктивнее) и строить отображения из одних языков в другие (семантические атрибуты и т.п.). Тут очень важный момент - в Sets мы не строим _модель_ языка в целом, мы просто определяем разные множества, разные конструктивные способы их построения и разные отображения между ними; для синтаксиса будут одни построения, для семантики - другие, для чего-то ещё - третьи. При переходе к Cats (1-категория) у нас языки это категории, уже не такие плоские как множества - есть типы как объекты и классы эквивалентности термов как стрелки, семантика при этом тоже (как и в Sets) даётся дополнительным построением - семантическим функтором. В 2-категории всё ещё более проясняется - язык как 2-категория это уже _модель_ с типами как объектами, термами как стрелками и классами эквивалентности вычислений как 2-стрелками, и заданием такой модели язык определяется _полностью_ - типизация, синтаксис, семантика, равно как и всё остальное что можно сказать о языке как языке задаётся одной 2-категорией (т.е. моделью). А 3-категории это уже модели реализаций языков - типы-объекты, термы-стрелки, вычисления-2-стрелки и классы эквивалентности оптимизаций как 3-стрелки.

Ну давайте без что-нибудь. Назовите конкретную теорему о 2-стрелках в произвольно взятой категории и переформулируйте ее в рамках терминов предметной области.

«что-нибудь» это риторическая фигура тут. Есть конкретные теоремы о CR в CCC и not CR в CMC. Зачем это? Ну что бы ответить на вопрос о том будет работать CR в какой-либо квантовой версии LC или нет (когерентные и некогерентные варианты).

Просто в данном случае вы можете обойтись без типов, когда они не нужны.

Не, нельзя без типов :) Просто _вы_ не хотите привлекать типизацию (а с ней и логику).

Еще раз - вы заменили классическое полустраничное определение ламбда-исчисления

TC вроде знаком с «классическим» определением. Вопрос был в том как ехать дальше. Я предполагаю, что категорные модели тут могут быть весьма полезны - разные расширения LC легко задаются введением дополнительных определений в категории, к тому же, есть линейные модели LC, есть квантовые модели (и те и те - с моноидальными категориями).

не вполне внятным переводом на теоретико-категорный язык

Если не нравится - я привёл ссылку на вполне понятную формулировку.

причем изрядно усложнив изложение и навводив кучу лишних сущностей. Причем ничего к оригиналу не добавив (перевод он и есть перевод). В чем проявляется «удобство» в данном случае?

Без понятия. Если для вас это всё лишние сущности, то значит мы просто видим по-разному. Ну и то что для вас «оригинал» я вообще не принимаю во внимание, ещё раз - это не перевод, это просто такой способ изложения.

Пока что нигде кроме логики да топологии ее и нету

Логика, топология, квантовые вычисления (примечательно, что лекции Манина про них начинаются с изложения ТК), квантовая физика вообще (стараниями Баеза, например), современная геометрия, да мало ли что ещё.

Если про CS - любые пограничные дисциплины, т.е. там где CS встречается с логикой или с квантовыми вычислениями.

Метафора про молоток и гаечный ключ забавная, но абсолютно не релевантная. И вообще это ретроградничество. Давай не будем спорить - просто признаем что есть nPOV (n-category POV), которая имеет право на существование.

> И где во втором предложении указание на операционную семантику?

Для типизированного лямбда-исчисления с полиморфизмом существует только одна операционная семантика. Если семантику поменять - это будет уже какая-то другая система.

> Почему нельзя использовать для этого множества?

Можно. И задают ведь спокойно :)

(задаётся только множество термов, а все структурные свойства

А все структурные свойства - это тоже множества, т.к. ничего кроме множеств в теории множеств нет. Другое дело, что для теории множеств вы можете отказаться от ассемблера и писать на ЯП высокого уровня.В теоркате кроме ассемблера способов описания нет. По-этому бОльшая часть объектов более точно, лаконично и естественно выражается именно в рамках теоретико-множественного подхода. Задание свойств конкретной 2-категории - это точно такие же «сторонние» построение.

Множество это объект 0-категории, это «плоская» и невыразительная конструкция. Если использовать объекты n-категории как модели - можно выразить гораздо больше.

Еще раз - формализмы строго эквивалентны. Вы всегда можете перевести любое утверждение туда-обратно. Нет никакой существенной разницы между «возьмем множество, удовлетворяющее условиям A, B, C и будем его исследовать» или «возьмем категорию, удовлетворяющую условиям A, B, C и будем ее исследовать». Речь идет лишь о том, что те или иные объекты в зависимости от _конкретной ситуации_ и от _конкретного контекста_ более удобно исследовать в рамках того или иного подхода. Но сам по себе (без указания контекста) ни тот ни другой подход не имеет каких-либо преимуществ. В силу эквивалентности.

Я не знаю что такое «эквивалентен», формально, так что ничего не могу возразить.

Ну еще раз - вы можете изложить теорию категорий в рамках теории множеств, уже тем самым любое теоретико-категорное утверждение автоматически становится утверждением теоретико-множественным. И наоборот. Вы говорите «множество - это бедная категория, т.к. мы можем задать категории куда более интересные». Аналогично можно возразить, что категория - это бедное множество, т.к. мы можем задать множества куда более интересные.

Вообще, чем ниже порядок категории, тем больше «лес» изучаемых структур будет скрываться за «деревьями» частных математических манипуляций.

Да нет же, это зависит от конкретного контекста. В одних случаях - это так, в других - «лес» изучаемых структур будет теряться за навороченными категорными конструкциями, хотя они там и не нужны. Это разные подходы и в разных ситуациях удобен либо тот, либо другой.

получается очень плоско и неконструктивно, структура языка никак не задаётся его множеством

Смотря что вы собираетесь понимать под языком.

Тут очень важный момент - в Sets мы не строим _модель_ языка в целом, мы просто определяем разные множества, разные конструктивные способы их построения и разные отображения между ними;

Аналогично в теоркате - мы не строим модель языка, мы просто определяем разные категории с определенными свойствами. Понимаете? В первом случае - мы определяем множества с определенными свойствами, во втором - категории с определенными свойствами. Подход строго симметричен, но вы никак не собираетесь этого понять. С точки зрения формальной логики - и теория множеств и теория категорий это просто две эквивалентные аксиоматические теории, построенные поверх логики первого порядка. И утверждения в них формулируются совершенно одинаковым образом.

> В 2-категории всё ещё более проясняется

«2-категория» - это категория, удовлетворяющая определенному ряду свойств. То есть это частный случай 1-категории, которая является частным случаем вашей плоской 0-категории (любая категория более «высокого» уровня есть частный случай категории более «низкого»). У нас в математике вообще нет никакого способа что-то определить, кроме как «возьмем объект общего характера, существование которого постулируется аксиоматически, и будет добавлять свойства, пока не решим, что хватит». И в общем случае нет ни малейшей разницы берете ли вы обычное бедное на свойства множестве и ограничиваете его или берете обычную бедную по свойствам категорию и ограничиваете ее. Это де-факто равносильные подходы, но вы просто в силу субъективности восприятие ограничение множества свойствами считаете чем-то «внешним», а ограничение категории - «внутренним».

«что-нибудь» это риторическая фигура тут. Есть конкретные теоремы о CR в CCC и not CR в CMC. Зачем это? Ну что бы ответить на вопрос о том будет работать CR в какой-либо квантовой версии LC или нет (когерентные и некогерентные варианты).

Мне кажется, вы не читаете, что я пишу. Я же просто попросил привести конкретную теорему и ее перевод на термины предметной области.

Не, нельзя без типов :)

Я вам уже показал, что можно. Выделяете id-стрелку и типов нет.

Если не нравится - я привёл ссылку на вполне понятную формулировку.

Просмотрел ваши посты - не нашел. Может, еще раз кинете?

Без понятия. Если для вас это всё лишние сущности, то значит мы просто видим по-разному.

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

Логика, топология, квантовые вычисления (примечательно, что лекции Манина про них начинаются с изложения ТК), квантовая физика вообще (стараниями Баеза, например), современная геометрия, да мало ли что ещё.

Я же там специально пояснил - подразумевалось, что она нигде кроме логики и топологии не используется иначе чем «переформулируем то, что уже есть».

Давай не будем спорить - просто признаем что есть nPOV (n-category POV), которая имеет право на существование.

Так я вам это и пытаюсь разъяснить. Есть теоркат, есть теория множеств. Это разные инструменты, которые удобно применять в зависимости от ситуации. Но гаечным ключом следует откручивать гайки, а молотком - забивать гвозди. И наоборот делать все же не стоит.

Для типизированного лямбда-исчисления с полиморфизмом существует только одна операционная семантика.

Может быть, но к этому утверждению она не относится никак вообще.

«2-категория» - это категория, удовлетворяющая определенному ряду свойств.

Это, разумеется, не так. Это более богатый объект, а не частный случай. Скорее наоборот: 1-категория является частным случаем 2-категории.

У нас в математике вообще нет никакого способа что-то определить, кроме как «возьмем объект общего характера, существование которого постулируется аксиоматически, и будет добавлять свойства, пока не решим, что хватит».

Что, однако, не означает, что из двух объектов один обязательно является частным случаем другого.

Несмотря на то, что подход эквивалентен.

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

подразумевалось, что она нигде кроме логики и топологии не используется иначе чем «переформулируем то, что уже есть».

А гомологическая алгебра - это логика или топология? В ней без категорного языка вообще никуда. Тот случай, когда используя более бедный язык (теормнож) цели не добиться вообще.

> Может быть, но к этому утверждению она не относится никак вообще.

Как она может к нему не относится, если истинность этого утверждения как раз от операционной семантики и зависит?

> Это, разумеется, не так. Это более богатый объект, а не частный случай. Скорее наоборот: 1-категория является частным случаем 2-категории.

Как раз нет. Из всех 1-категорий можно выбрать 2-категории, наложив на 1-категории ряд ограничений. Да и давайте так - если вы говорите, что 2-категория не есть частный случай 1-категории, то назовите свойства 1-категории, которым 2-категория не удовлетворяет. В 2-категории стрелки есть? Есть. Единичиные стрелки есть? Есть. Композиция определена ассоциативно? Да. Больше для категории ничего не требуется. Вывод - это категория.

Что, однако, не означает, что из двух объектов один обязательно является частным случаем другого.

Если объект А - это объект Б, на который наложен ряд ограничений, то А - частный случай Б. Как 2-категория частный случай 1-категории.

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

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

А гомологическая алгебра - это логика или топология?

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

В ней без категорного языка вообще никуда.

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

Тот случай, когда используя более бедный язык (теормнож) цели не добиться вообще.

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

если истинность этого утверждения как раз от операционной семантики и зависит?

Если операционная семантика одна, то зависеть от неё что-либо не может. Зависимость появляется, только когда что-либо меняется.

Из всех 1-категорий можно выбрать 2-категории, наложив на 1-категории ряд ограничений.

Нельзя. 2-стрелки из ниоткуда не возьмутся. Нужно не только накладывать ограничения, но и добавлять структуру.

В 2-категории стрелки есть? Есть. Единичиные стрелки есть? Есть. Композиция определена ассоциативно? Да. Больше для категории ничего не требуется. Вывод - это категория.

Да. Но это не значит, что 2-категория - частный случай категории. Ибо могут быть РАЗНЫЕ 2-категории с одинаковыми классами объектов и 1-стрелок.

Прошу прощенья, рановато кнопку нажал.

Если объект А - это объект Б, на который наложен ряд ограничений, то А - частный случай Б.

Да.

Как 2-категория частный случай 1-категории.

Нет.

И вот как раз здесь у теории множеств плюс - для нее высокоуровневые языки написани.

Один такой называется «теория категорий».

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

Подавился бубликом. То есть, вы считаете, что гомологии групп, колец, алгебр и те пе относятся к топологии?

теория категорий это _и есть_ гомологическая алгебра, если уж смотреть в историческую перспективу.

Нет, конечно. Теория категорий НАЧАЛАСЬ с гомологической алгебры.

Опять-таки, говорить так некорректно просто потому, что теоркат можно сформулировать в рамках теормножа.

А Эрланг можно написать на C. Но свою технику Эриксоновцы на Эрланге запрограммировать смогли, а на C - нет.

Кстати, в рамки ZF теория категорий не укладывается.

> Если операционная семантика одна, то зависеть от неё что-либо не может.

кто сказал, что она одна?

кто сказал, что она одна?

Анонимус, чуть выше.

> Нельзя. 2-стрелки из ниоткуда не возьмутся.

Они там и так есть, им не надо браться. Вообще говоря, у нас есть лишь совокупность стрелок, категорию (n-категорию) мы получаем, когда вводим над этими стрелками операции, и накладываем на эти операции ограничения. Точнее, это будут не операции, а функциональные символы (в смысле формальной теории).

Да. Но это не значит, что 2-категория - частный случай категории. Ибо могут быть РАЗНЫЕ 2-категории с одинаковыми классами объектов и 1-стрелок.

Нет, не могут. 1-категории тут совпадают _с точностью до изоморфизма_. Но для _разных_ (не с точностью до изоморфизма - а вообще разных) 2-категорий мы имеем различные 1-категории. Да и вообще неясно. Если мы говорим о теории множеств, то в теории множеств есть только множества. И любая 2-категория - это просто такое множество (которое надо выбрать из других множеств, накладывая ограничения). Если мы говорим о теории категорий, то в теории категорий есть только стрелки. И любая 2-категория (как и 1-категория) - это такая стрелка. Которую надо выбрать из других стрелок, наложив соответствующие ограничения.

Ю Анонимус, чуть выше.

Она одна для простого типизированного лямбда-исчисления. Но вы конкретную систему в своем посте не упоминали.

Они там и так есть

Где именно?

Нет, не могут. 1-категории тут совпадают _с точностью до изоморфизма_.

Ошибаетесь, могут. В том числе - полностью совпадающие, а не «с точностью до».

И любая 2-категория - это просто такое множество

Нет. Категория может не быть множеством вообще. Собственно, как правило, и не является.

И любая 2-категория (как и 1-категория) - это такая стрелка.

А вот это уже просто чушь.

Она одна для простого типизированного лямбда-исчисления.

А следовательно, зависеть от неё что-либо не может. QED.

> Нет.

Нет ну как нет если да? 2-категория получается из 1-категории введением дополнительных ограничений на совокупность стрелок.

Один такой называется «теория категорий».

Если говорить о теоркате в рамках теории множеств - да. Если говорить как об отдельной формальной теорий (о чем, вроде, речь и шла) - конечно, нет.

Подавился бубликом. То есть, вы считаете, что гомологии групп, колец, алгебр и те пе относятся к топологии?

Давайте по порядку. Изначально теория гомологий была разделом алгебраической топологии (с этим, надеюсь, спорить не станете), потом ее методы начали применяться в других разделах математики. Если у вас результаты теории групп применяются, ну, например, в той же дифференциальной геометрии, теория групп перестает быт теорией групп и становится геометрией, или как?

Нет, конечно. Теория категорий НАЧАЛАСЬ с гомологической алгебры.

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

Кстати, в рамки ZF теория категорий не укладывается.

Нам ведь и не надо обязательно в ZF.

> Нет. Категория может не быть множеством вообще.

Если говорить о категориях, которые можно задать в рамках ZFC - множество. Но вообще да, тут зависит от аксиоматики.

А вот это уже просто чушь.

То есть в рамках теории категорий такое понятие как «категория» сформулировать нельзя, я верно понял ваше утверждение? Потому что если можно - это неминуемо будет стрелкой. Потому что в теоркате _нету_, вообще _нету_ никаких объектов кроме стрелок. «объект» - в смысле значение пропозициональной переменной.