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)
шерстяной ленин

July 2017

S M T W T F S
       1
2 3 4 56 7 8
9 1011 12 13 14 15
161718 19 2021 22
23242526272829
3031     

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 22nd, 2017 06:46 pm
Powered by Dreamwidth Studios