sea

FAQ #2 по Groupoid Infinity

1. Я слышал, что верификация критоповлют и их языков достаточно сложная тема. Ведь чтобы верифицировать язык и его модель — это уже нужно полностью ее загнать в Coq/Agda, а нужно ведь еще верифицировать компилятор или виртуальную машину, что она сохраняет свои свойства. Как вы это все собираетесь писать двумя человеками?

Если идти таким путем, который описан в вопросе, то может выглядеть действительно сложно. Однако мы сторонники PCC подхода, где теоремы (свойства) поставляются в том же языке на котором написан исполняющийся код. В нашем случае — это OM. Другой пример такой платформы как идеи распространения trusted кода по Internet — это Morte. В ACL2 (прувер для инженеров) тоже код экстрактился в Common Lisp вместе с проверками свойств.

Наш подход немножко другой чем предоставление Сертифицированной Виртуальной Машины, Языка Контрактов и его Сертифицированного Компилятора. Вместо этого мы предлагаем писать на DSL с зависимыми типами (кванторами) а виртуальной машиной будет служить виртуальная машина Erlang, достаточно надежная если работать в ней без эффектов. Код лямбда ядра OM будет превращаться в код исполнительной среды. Терминированность обеспечивается самим тайчекером и теоремами которые поставляются вместе с кодом и чекаются на стороне сервера.

Этот подход подразумевает распространение микропограмм на чистой лямбде в качестве трастед виратуальной машины (никто ведь не будет спорить что лямбда кор более трастед чем любая штука, которую могут придумать люди, добавив свою extra complexity для решения теоретических сложностей или технический сложнойстей (производительности). ОМ и есть трастед виртуальная машина, имплементацию которой подменяет subset Erlang, который может только лямбды апплицировать. Верифицировать такую машину проще, чем кастомные машины для контрактов.

Но мы не только не разрабатываем виртуальную машину, мы также не особо разрабатываем язык контрактов. Для нас это разработка языка с зависимыми типами EXE с компактной библиотекой в духе Elm, а прикладные задачи (пакетные фильтры, бизнес контракты) — это просто DSL на этом языке. Все эти прикладные задачи описывают алгоритмы которые экстрактятся в lambda core, инкрустированные универсальными квантификаторами.

2. Я слышал что в любых системах нужно писать Unit тесты. Даже когда вы доказываете свойства систем. Может ваша система доказать мой код на Scala/C# ?

Ну давайте посмотрим как повышают качество ПО:

— Unit tests
— TDD/BDD
— Property testing
— Formal Methods

Мы работаем в контексте последнего пункта — формальных методов. Наш продукт не является системой похожей на QuickCheck ни более того никак не связан с тестированием фунционального и семантического наполнения ваших моделей. Т.е. мы пока не строим модели на заказ (пока не было заказов), а разрабатываем инфраструктурные элементы системы исполнения и редистрибюции верифицированного кода, который проходит тайпчек — как если бы это были сертификаты, которые совпадают с наперед сформулированными теоремами свойствами. В этих свойствах вы можете например лимитировать время тайпчека или размеры выделяемой памяти в процессе его работы.

Но для этого нужно использовать язык с кванторами. Т.е. пока вы не используете кванторы — вы просто занимаетесь композицией аксиом MLTT. При этом вы можете продолжать оставаться в System Fw, но как только вы захотите доказать какое-то свойство ваших конструкций, вам придется выйти в зависимую теорию, и ваш код при этом будет похож на Coq/Agda/Lean. Т.е. без кванторов — это должен быть обычный язык уровня ML или начальных Haskell-ов — с минимумом конструкций, только с record (они же модули) и data. Паттерн мачинг понятный эрланг программисту и дюжиной примитивов в базовой библиотеке для построение систем, которые обычно строят на платформе Erlang/OTP.

3. Почему ядро без Sigma, Equ, Fix/Rec?

Мы можем также взять переписать тайпчекер Lean из Хаскеля на эрланг и получить новый байткод и новое лямбда ядро, совместимое например с Lean, но мне показалось, что чем проще ядро — тем более к нему доверия можно вызвать у индустрии. OM реально доступен любому инженеру для понимания. Сложные пруверы с большим ядром требуют объяснения. Возможно будут и другие ядра, но пока идея с OM ядром очень интересна, так как в ней возможно вычисление лимитов начальных алгебр, а значит вы можете использовать индуктивные типы и весь инструментарий на котором сформулированы все современные теоремы.

Наш язык не будет включать никаких тактик или чего-то похожего, так как это ведет к развувания ядра, а ощутимой пользы не приносит, приходится руками заниматься композициями высказываний в другом DSL. Зачем? Если можно было просто заниматься композицией высказываний в том же хост-языке и держать теоремы в носителях типов и значений, в рекордах. Такой рекорд с функциональностью и теоремами называется PCC и может редистрибуцироваться по ненадежным каналам. Idris например тоже изначально содержал язык тактик для интерактивного доказательства теорем, но потом его разработка была приоставлена, так как усложнялось ядро прувера.

4. Зачем мне еще один Coq?

Дело в том, что Coq — это язык для математиков, EXE — это язык для инженеров которые работают с буферами грубо-говоря. Нас интересуют пока только алгоритмы связанные со стримами или бесконечными/конечными списками и их процессиногом в условиях распределенной работы. И нас интересует максимально простая форма ПиСигма языка, которая была сравнима с тем, как Эрланг проще всех остальных языков.

Если этот язык и его базовая библиотека окажется слишком сложным в использовании (Например сложнее чем Хаскель или Scala), то мы будем считать, что наша задача не выполнена.

5. Одна из проблем существующих пруверов, как мне объяснили и как я понял - интерактивность. То есть они все требуют каких-то отношений с живым человеком, чтобы правильно все проверить. Будет ли у вас так же или будет возможность в одну трубу закинуть код, в другую какие-то параметры, и получить ответ на выходе?

Мы не продаем никакой интерактивности. Конечно у нас будет pretty print colored eval (just like in Elixir, потому что мы по сути просто еще один Erlang язык), но так как в языке нет тактик для рабочего матемаика, то это скорее язык для инженеров. А инженеров не заставишь писать алгоритмы в графических редакторах (именно поэтому пока в BPE отсувствует векторный редактор Workflow). Никакой магии наш прувер не предоставляет, это все лишь (в порядке увеличения крутости поставленных целей):

— просто нормальный Хаскель для Erlang
— ядро прувера
— top-level язык Erlang с родным экстрактом и биндингами (маршалингом) типов Erlang
— библиотека теорем для хранения цепочек
— библиотеки для распределенного алгоритма чейн репликация
— криптовалюты, блокчейн и т.д.

6. Есть ли какой-то способ с помощью OM/EXE верифицировать не только код, на нем написанный, но и код на других языках?

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

Как правило сейчас на рынке все хотят верифицировать С код. Мы не соревнуемся на этом рынке никоим образом, и наш подход полностью исключает такую модель построения доказательств. Если вы хотите ферифицировать C код, вам нужно взять VST CompCert С компилятор, написанный на Coq, преобразовывать С программы в Coq листинги и работать уже продолжать в Coq. Мы считает такой подход полным фейлом, та как это требует отдела R&D для выполнения это работы. Вы конечно можете нанять консультантов, ребята из http://www.functor.se вам все сделают за дорого, там лично у них советник Альтенкирх http://www.functor.se/company/leadership/

Мы поставщики совершенно другого подхода. Мы предлагаем тоже платформу но в которой доказательства строятся не через доказательство изоморфных экземпляров теорий, а вытаскивается в target язык напрямую из описание программы написанной на EXE, который мы хотим сделать engineer friendly. В идеальном случае, предствате, что все типы в нашей базовой библиотеке поставляются с основными теоремами и вы просто пишете какой-то сетевой код или сервисы для стриминг процессинга используя этот Haskell для Erlang, как обычный программист, не задумывясь особо о построении метамодели. Потом математик просто проставляет PCC, или мы наперед пишем программы исходя из заданных PCC. Важно тут что для программиста — это должно выглядеть как еще один Elixir с кванторами и странным синтаксисом или Elm с бекендом в Erlang вместо JavaScript.
Buy for 10 tokens
Buy promo for minimal price.
sea

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

Я не понимаю, в чем идея камента Хуана Ганди, но суть вроде такая, что запретительная статья дла λP2, а λPω такая статья не запрещает, а у нас не просто λPω=CoC (с двумя вселенными), а с бесконечным их количеством. Если Хуан Ганди считает мое мнение аргументации (я не говорю о мотивации постановки задачи), пусть потрудится указать на ошибку в моих логических рассуждениях о возможной поставке проблематики (я не говорю что у меня есть готовое решение). Но запретительной статьи именно на невозможность построение терма индукции (или Sigma типа выраженного только на Pi) в CoC + predicative hierarchy of universes, насколько я знаю не существует. Или, если он возьмется за $100/час на 4 часа ее расписать (показать что не существует во всех кодировках, чтобы это не была белетристика или Дилберт в картинках), я с радостью заплачу назамедительно сумму (за 4 часа) и признаю что я нижайший пидоро-червь на планете :-)

Вот линк статьи:
http://www.cs.ru.nl/~herman/PUBS/IndNonder.ps.gz

Это опрос. Просто заходите и пишите в комментариях номер

0 — Я верю и желаю Максиму удачи
1 — Нет я неверю, я просто хочу заявить об этом сдесь в журнале и всему миру
2 — Я знаю, что это невозможно, и ставлю Бид 400 баксов, что это невозможно, когда покажите кодировку, где это возможно, я перечесляю деньги сразу на любой счет мира. Другими словами я настолько уверен в правоте, что каждое мое заявление об этом равносильно 400 баксам и я кричу об этом на весь интернет, во всех комментариях и т.д.
3 — Я думаю, что это невозможно и просто зашел проголосовать за этот пункт
4 — Я за N* баксов показываю почему это нельзя сделать, и это подтверждает любой независимый математик консультант, который устроит обе стороны приема-передачи баксов и доказательства. Если таковой найдется, то он тоже должен написать за какую сумму он готов совершить разбор полетов, чтобы это все было должным образом освидетельствовано.

Если б таких громко кричащих неверующих найдется как Хуан Ганди, хотя бы три. Я не говорю что это хуйня деньги, но я поставил больше чем 400 баксов, там считали в каментах, буду транкейтить все что после запятой 2000 баксов. Больше просто нет. Будет больше поставлю больше. Если кто-то хочет доказать хоть что-то, чтобы это не была хуйня — пожалуйста! Я буду платить Ганди за любое нетривиальное доказательство чего бы то ни было, чтобы при этом был какой-то арбитр. Вот например Андрей. Но я так понимаю заявление Хуана Ганди по сути означает что ебанат не только я, но и Паша и Андрей, раз они что-то делали по этому поводу. Так что если кто-то хочет выступить в роли арбитра, я готов заплатить денег и найти их для этого. Довольно честное предлолжение. И ставки и спор, настоящая игра для обеспечения деятельности математиков.

P.S. Вот кстати скомпилированная индукция:
> ls(ebin).
Bool.beam                          Cmd.beam
Data.Bool.Alg.Id.beam              Data.Bool.Alg.Mul.beam
Data.Bool.Alg.Ob.@Carrier.beam     Data.Bool.Alg.Ob.@False.beam
Data.Bool.Alg.Ob.@True.beam        Data.Bool.Alg.Ob.beam
Data.Bool.Alg.beam                 Data.Bool.Endo.beam
Data.Bool.EndoSet.beam             Data.Bool.IId.beam
Data.Bool.Init.=False.beam         Data.Bool.Init.=True.beam
Data.Bool.Init.beam                Data.Bool.Predicate.beam
Data.Bool.SInj.beam                Data.Bool.Sigma.=False.beam
Data.Bool.Sigma.=True.beam         Data.Bool.Sigma.beam
Data.Bool.beam                     Data.Bool.recur.beam
Data.Bool.recur.forHom.beam        Data.Bool.recur.forId.beam
Data.Bool.recur.forOb.beam         Data.Bool.recurP.beam
Data.Bool.recurP.forOb.beam        Data.Empty.Alg.Id.beam
Data.Empty.Alg.Mul.beam            Data.Empty.Alg.beam
Data.Empty.beam                    Data.beam
Frege.beam                         IO.beam
IOI.beam                           List.beam
Maybe.beam                         Mon.beam
Monad.beam                         Monoid.beam
Morte.beam                         Nat.beam
Path.beam                          Prod.beam

$ ls -l Data.Bool.beam
-rw-r--r--  1 5HT  staff  109144 Aug 22 13:06 Data.Bool.beam


Занимает 106.5859375KiB. Из которых рекурсор занимает:

$ ls -l Data.Bool.recur* | awk -F " " {'print $5'} | awk '{s+=$1} END {print s}'
98876


99КБ.
sea

Заявление от Групоид Инфинити

Закон причины и следствия — безошибочен


У всех бывают кризисы, не обошли они стороной и Групоид Инфинити. В интернете уже пошли слухи среди математиков, что якобы Групоид Инфинити не выплачивает зарплат и к нам не стоит идти на работу. Рано или поздно эта информация расползется по интернету, поэтому, во избежание недоразумений, хотелось бы четко объяснить свою позицию, поскольку прозвучали личные обвинения в мой адрес. Чтобы понять суть любого конфликта, так или иначе придется рассказывать полную историю, чтобы были видны причины воплотившихся последствий.

В конце 2015 года, я, с подачи Влада, решил портировать Morte на Erlang, для того чтобы попробовать сделать игрушечную кодировку Беррардуччи. Я влюбился в базовую библиотеку Morte и наконец увидел своими глазами, что ядро прувера можно сделать на 300 строчек, при этом имея систему эффектов и более-менее современную библиотеку.

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

Я посоветовался с известными математиками, в том числе и с моими наставниками, которые учили меня теории категорий (в свое время), и с которыми мы хостили соотвествующее коммюнити category_theory в ЖЖ. Они меня предупредили, что Паша — человек специфический, поскольку, как и все математики, обладает незаурядным мышлением. Меня это воодушевило и я решил предложить Паше действительно интересную задачу — трансляция CiC в CoC. Многие люди мне говорили, что задача эта непосильна, а некоторые даже прямо утверждали, что это невозможно. К счастью, серией кратких бесед в моем стиле, пробивающем сразу в суть, я убедил Пашу, что это возможно, мы пригласили (в качестве консультанта со стороны) Андрея и начали работать. (Напомню, что были найдены запретительные публикации на эту тематику и нужно было быть действиетельно смелым, чтобы погрузиться в работу, которая уже считается невозможной и есть на эту тему публикации).

С самого начала наше сотрудничество никоим образом не могло восприниматься, как руководитель-подчиненный, я называю — это компенсациями, потому что у нас не было ни формального плана работы, ни полноценных трудовых отношений, я просто перечислял (малые по меркам программистов) деньги Паше, зная и понимая его тяжелое финансовое положение; по большому счету мне было все равно, чем он занимается, так как его познания в этой области гораздо, гораздо превышают, не только мои, но 99% всех людей, которые могут что-то понять из этой работы.

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

Все шло хорошо и мы даже записали подкаст с Пашей https://soundcloud.com/maxim-sokhatsky/omexe-podcast, анонсируя совместно прототип рабочей кодировки на "Первом Категорном Митапе" в Июне http://synrc.com/news/2016/groupoid.htm. Я не стал подганять Пашу и мягко отвечал в письмах читателей: "мы работаем, следите за новостями", которые меня постоянно спрашивали про новую дату этого митапа.

Так сложилось, что моя финансовая ситуация изменилась, в связи с окончанием и успешой сдачей проекта в ПриватБанке (напомню, что мы перевели 3 большие вкладки в Приват24 посвященные депозитам на наш веб фреймворк N2O, состоящие из 100 бизнес процессов на нашем BPE, и около 300 форм на NITRO и наших DSL) и организацией большого мероприятия, в которое я вложил все оставшиеся деньги, о чем я неоднократно говорил Павлу. Поэтому я попросил в конце мая Андрея выплачивать деньги Паше, чтобы поддерживать его, поскольку я больше не мог это делать. По большому счету окончание сотрудничества с ПриватБанк связано с моим искренним желанием работать над Erlang прувером, и верой в успешность этого проекта, так как ПриватБанк не захотел поддерживать или финансировать, пускай транзитивно, в этот проект. У меня даже случился конфликт с женой, так как я перечислил Паше тогда последние деньги со своего счета.

Когда я вернулся из ритрита, я узнал, что у Паши есть определенные результаты, и я наконец увидел шаблон индукции, который похож на классическую индукцию. По пути Паше потребовалось три раза сменить кодировку: с Setoids, до Posets и потом до рафинированой и упрощенной с кодовым названием Simpleton. Меня Андрей попросил вернуться в проект и помочь Паше, актуализировав наши цели, как получение рабочей кодировки, не размазывясь "мыслями по древу". Так как уже был виден шаблон и можно было начинать непосредственную работу по кодированию.

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

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

Из всей этой истории я усвоил для себя серию уроков:

1) не нужно вкладывать последние деньги в проекты;
2) не нужно помогать людям, не получая ничего взамен (должно всегда быть два блага: одно для себя, и второе — для других);
3) не нужно делать старап с людьми, которые не доверяют тебе полностью;
4) я усвоил также, что наш хипстерский подход (без обязательств, планов, сроков и отчетов) в управлении проектами не работает с математиками, для математиков нужна ясность и четкая определенность.

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

P.S. Я хочу сказать, и люди которые приходили ко мне на собеседование на этот проект не дадут соврать, что я очень уважительно отношусь к математикам. За собеседования я выплачиваю сразу 2000 грн, только за то что человек приходит на собеседование. Не важно будет он этим заниматься или нет, я всегда выплачиваю и уважаю время других людей. И обвинения, что я зажал деньги ни как не могут быть применены ко мне, ни в одной из существующих вселенных. Я продам машину и квартиру, но деньги выплачу.

В этом месте я включу режим "тупого руководителя", для Павла, чтобы он посмотрел на эту ситуацию с той стороны, какую он выбрал. Чисто гипотетически мы имеем то, что мы договорились, что я ему перечисляю "на еду" (как он выразился деньги) в размере 2000 грн в неделю. С начала года прошла 31 неделя и было выплачено 65,149 грн. Получается 2101,5 копеек. Т.е. я выполнил и превысил размер своих обещаний.



Взамен я не получил алгоритм кодировки, который был бы понятен условному Кметту. Павел говорит, что у него он в ЖЖ, но собирать по его постам из ЖЖ алгоритм категорного кодирования CiC в CoC — это та еще олимпиада, я это делал, и все, что у меня получилось — это мои PDF документы в каталоге EXE/DOC. Я увидел только термы (которые не парсаются) записанные на ОМ в двух промежуточных кодировках и ни одного законченного терма в финальной кодировке. Так же я увидел от Павла модифицированный тайпчекер ОМ (которым мы заменили тайпчекер Гонзалеза). Это все что я увидел от Павла.

Мы задержали митап на 3 месяца и теперь становится ясно, что его не будет. У меня в режиме ON-HOLD находится несколько переписок связанных с моими просьбами по финансированию проекта на более солидном уровне, но к сожалению я вынужден написать это письмо, чтобы люди, которые раздумывают о вложении в проект, видели всю ситуацию открыто. Возможно, они поверят в меня и решатся на финансирование, тогда я буду искать людей, которым это было бы интересно, но это уже будет по совершенно другим правилам.

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

Наноядра чистый изумруд

В Твиттере пошла волна репостов про https://github.com/littlekernel/lk Но среди молодняка мало кто знает, что автор этого ядра Тревис Гейзельбрехт был со-автором ядра операционной системы BeOS, а также автором NewOS, которое фактически в неизменном виде стало основой HaikuOS. Теперь Google начало пилить Фуксию, ОС основанную на LK. Все-таки BeOS выстрелил! Also если кто незнает из NewOS известный ебанат Дима Завалишин понадергивал кусков и всем говорит что заебашил PhantomOS с нуля.

Я когда-то дико упарывался по BeOS, Haiku и даже ебашил там на С++ чаты и KHTML портировал с KJS. Но теперь у меня смешанные чувства: с одной стороны я рад, что правительство Гугла дало добро на закапывание Линукса, с другой я уже перерос это байтойобство. Только лямбдочку хардварную верифицировнную мне подавай. К старости говорят все капризными становятся как дети.

Таки дела, пацаны.
buka

Порядок редукций и Элиминатор Bool

Поднял из анналов, старый тред akuklev, nponeccop и udpn про if и "заходить в две ветки"

http://udpn.livejournal.com/78084.html

Напомнимаю, что мы все у себя давно померяли, для нормализации/ненормализации, eager/lazy вариантов:

http://maxim.livejournal.com/471966.html

Наткнулся на фразу

> В extensional ITT существуют сетоиды, но это жалкая замена левой руки.

Интересно что имелось ввиду? Что круто писать на J элиминаторе все, как на предыдущих слайдах? :-)
sea

Identity Types in EXE





____________________
[1] E.Bishop Foundations of Constructive Analysis 1967
[2] T.Streicher, M.Hofmann The groupoid interpretation of type theory 1996
[3] G.Barthe, V.Capretta Setoids in type theory 2003
[4] M.Sozeau, N.Tabareau Internalizing Intensional Type Theory 2013
[5] V.Voevodsky Identity types in the C-systems defined by a universe category 2015
[6] D.Selsam and L.de Moura Congruence Closure in Intensional Type Theory 2016
buka

MONADS NEED NOT BE ENDOFUNCTORS

We will elsewhere comment on the relation of our relative monads to the recent gen- eralization of monads by Spivey [31] that was also motivated by programming examples: he fixes a functor K ∈ C → J (notice the direction) to then look for monad-like structures with an underlying functor J → C. With Paul Levy we have checked that a fair amount of monad theory transfers to his generalized monads, but they are not monoids in [J, C] unless K has a left adjoint, in which case they are equivalent to relative monads. Sam Staton has considered an enriched variant of relative monads.

http://jmchapman.github.io/papers/relmon-lmcs.pdf

Кто еще раз пизданет что Монада — это моноид в категории эндофункторов, сразу с вертушки :-)
sea

Благословение от Хенка получено

Henk Barendrecht wrote:

Dear Maxim,

1. Great that you have reached a point in your software
development where you need automated verification
via formalization. Indeed you have my blessings.
My co-author and former colleague Freek Wiedijk
will almost for sure be interested in your project.
He is not happy with the existing provers and has
reimplemented automath.

...


Работаем дальше!
sea

Собеседование в Групоид Инфинити

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

Итак, как вы знаете мы работаем в чистейшем как слеза CoC, с бесконечными наобором аксиом для вселенных. Разные конфигурации у нас возможны, предикативные, импредикативные, внизу одна импредикативная для Prop как у всех и.д. Комулятивные эмулируются, так что для простоты они не нужны.

Так вот для статьи я начал выписывать семантику. Ну ее еще Мартин Леф выписал в 1972 для Пи типов, т.е. наш ОМ. А потом уже идет семантика EXE.

В EXE дальше идет у нас равенство с J элиминатором. В 1988 году была записана семантика для теории категорий (наша рабочая теория) в теории типов Мартина Лефа. Потом была записана семантика для Well Founded Trees, которые полиномиальные функторы, они же индуктивные типы в общем случае, ну а дальше идут высшие индуктивные типы. Как выписать Type Inference Judgment Rules для скажем Транкейшина или Гомотопической Сферы — тривиальная задача, которую может выполнить даже такой дибил как я. А в команду мы возьмем того, кто выпишет правила вывода для высших индуктивных типов в общем случае (HIT-form, HIT-intro, HIT-elim, HIT-comp).

Ждем ваших писем! :-)