bamalip: (NGE)
прикидывал сегодня на листочке, что у нас уже есть в высокоуровневом виде [1], что надо перенести в низкоуровневый и в какой последовательности [2] (с одной стороны), и (с другой) что нам пока предстоит написать и там и там для предикативного случая.

[1] https://github.com/groupoid/exe/blob/master/prelude/lean/Initial.lean
[2] https://github.com/groupoid/om/tree/master/priv/new-setoids

Во-первых, оказывается, что оттранслировать напрямую определение категории в таком виде нельзя "одно на все случаи", не только ввиду нереализованности universe polymorphism (который скоро будет), а более потому, что понятие "тип" в высокоуровневом представлении требуется транслировать в понятие "контекст", под которым в ТТ понимается то, что можно записать слева от штопора - последовательность переменных, типы которых могут быть взаимно зависимы. Главным примером является "сетоид", который задается таким контекстом. Мы сейчас называем это простой кодировкой типа record каррированными аргументами, но по-научному это надо называть "контекст" :) Так вот, определение категории необходимо инстанциировать не только для разных универсумов вида *n, но и для различных последовательностей универсумов, определяющих вид контекста (в данном случае, задающих сетоид). Такая форма специализации определения слишком сложна, и ее, скорее всего, нет смысла засовывать в низкоуровневый язык, самое место для нее - в промежуточном языке макросов. С другой стороны, в высокоуровневом ЕХЕ необходимости в ней нет, потому что механизм сетоидов нам обеспечит кодирование произвольных индуктивных типов, и нужен будет единственный вид контекстов, - те, что определяют сетоид.

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

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

Profile

bamalip: (Default)
шерстяной ленин

September 2017

S M T W T F S
      1 2
3 4 5 6 7 8 9
1011 12 13 14 1516
1718 19 20212223
24252627282930

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 21st, 2017 05:34 pm
Powered by Dreamwidth Studios