Само по себе — норм, но мы обсуждаем функцию, которая вычисляет термы не только нужного типа. 😊
Кроме того, с этим "остальные — пофиг куда" технически геморройно работать, поэтому лучше бы их все в одно место (0, none, undefined, whatever).
Я вот думаю над тремя вариантами:
• заменить ноль на option none
• в параметрах функции eval_nat требовать доказательство того что входной терм типизируется в nat_type
• ввести некий Tm_Error который не будет типизироваться и соответственно приводить к ошибке типизации.
Как будто второй вариант самый разумный, но как вы считаете?
Тупо проверять корректность построения терма с учётом наличия Tm_Conv в нужных местах — не вариант? Писать функции, которые проверяют всё, что нужно — перебор?
А, я понял почему я так халтурно написал эту функцию: я когда её писал не был уверен что вообще что то получится, ну и написал так сказать по минимуму, и что там вместе с Tm_Conv лежит тоже не стал проверять, мол всё равно пока кроме как с натами конв не используется. И t1 не проверял примерно по той же причине.
В общем вы правы нужно 0 заменить на option none и строго проверять термы по построению, не делая никаких допущений.
Благодарю!
Type Theory in Type Theory using a Strictified Syntax — крутая, интересная и релевантная статья, но для понимания всё равно требует знания дофига теории категорий. Интересно было бы её разобрать, но для начала нужно найти что-то ближе к основам.
A short technical summary for category theorists: although the ordinary presheaf model is not
strict enough for our purposes, if one starts with a strict category C 𝑠 , the category of subcoalgebras
of cofree presheaves on C 𝑠 is. The CwF structure on this category was defined by [Pédrot 2020] and
we call it PMP(C 𝑠 ). If C 𝑠 in addition is a (weak) model of type theory, then PMP(C 𝑠 ) has a universe
coming from the type formers in C 𝑠 . The telescopic contextualisation of this universe gives a new
strict CwF structure equivalent to C 𝑠 . The category part of any weak CwF can be strictified via the
full subcategory of PSh(C) spanned by representables. The construction in this paper first turns C
into C 𝑠 , and then uses PMP(C 𝑠 ) to obtain a new stricter model equivalent to C.
https://www.youtube.com/watch?v=dGvHmK4zu0k
В Ангиули CwF переупакованный на язык natural models, чтобы типы-конструкторы задавались простым декартовым квадратом.
Пробираться сложно, потому что цепочка конструкций для задания модели (presheaves → category of elements → slice → representability → pullbacks) наслаивается без введения базовых категорных определений и промежуточных диаграмм. В голове сложно даже одно определение держать. Зато для квадратов диаграммы есть, спасибо...😶
Можно, например, пробраться так: Ангиули держать за бейзлайн, отдельно уяснить возникающие категорные понятия, и при непонятных шагах обращаться к статьям где всё последовательно разжёвывается (внятные и последовательные источники-кандидаты отметила звёздочкой).
Если на этой неделе на созвоне разберём возникающие категорные понятия и пройдём 6.1 (или просто CwF), по-моему уже хорошо?
Для CwF особо много категорий не надо знать 🙂
CwF:
1*. [CATEGORICAL MODELS OF TYPE THEORY. AUKE BOOIJ AND DANIIL FRUMIN] внятно и последовательно, с диаграммами + примеры
2*. [TYPE THEORIES IN CATEGORY THEORY, TESLA ZHANG] сейм + введение категорных понятий
- [Towards Formalizing Categorical Models of Type Theory in Type Theory. Alexandre Buisse, Peter Dybjer] с формализацией на Агде
- [Internal Type Theory, Peter Dybjer]
- [Categories with Families: Unityped, Simply Typed, and Dependently Typed]
Natural models:
-* [Natural models of homotopy type theory, Steve Awodey] основная работа
-* [Abstract and concrete type theories, Taichi Uemura. ch.3; 5.3 slice theories]
-* [Algebraic models of dependent type theory, Clive Newstead, ch. 2]
_____
Про возникающие категорные понятия:
we shall assume familiarity with categories, functors, natural transformations, presheaves, the Yoneda embedding, and adjunctions
pullbacks, forgetful functor
- это было до 6-ой лекции по теории категорий включительно
- либо эти видео могут быть понятнее: [предпучки, вложение Йонеды] и [сопряженные функторы ч. 1, ч.2].
presheaves, yoneda lemma, fibers, category of elements of
Раз есть папира от Tesla Zhang — надо читать! 😁
Можно вообще попробовать с Теслой договориться о созвоне, если у него время есть. Чего может не быть, тем более он, поди, до сих пор в США, на пол-суток от нас.
Есть рац. предложение с моей стороны: в это воскресенье семинар пропустить, а к следующему прочитать статью Теслы — мне очень нравится, хорошие диаграммы, отличная подборка материала — и сколько успеем из 6 главы — 2-3-4 раздела. По сути, там один и тот же материал, просто Тесла объясняет "для дураков", а Грацнер с Ангиули введение ещё не написали.
@lbdlbdlbdl@anton0xf что скажете?
Вот я занимаюсь формализацией своего детища в Rocq.
Подскажите пожалуйста (направьте) как сохранять баланс между:
1) формулированием всяких отношений и синтаксисов (индуктивное отношение типизации/вычисления, синтаксис типов/термов, функции вроде infer, eval.
2) Доказательством свойств моей системы.
Меня кидает со стороны в сторону — чему стоит на данном этапе уделять больше внимания? Или стоит делать 50/50 ?
С одной стороны, Вы пока доказываете какие-то тривиальные и, в целом, бесполезные свойства, но с другой, никакие полезные Вы "с наскока" всё равно не докажете (без ИИ), — нужно на чём-то тренироваться. Так что если Вам до сих пор не надоело доказывать тривиальные теоремы, значит, ещё не научились, можно продолжать в том же духе. Когда надоест — усложняйте систему и переходите к более интересным свойствам.
Я думал, что полнота вывода типов и разрешимость равенства это хоть сколько-нибудь интересные и полезные свойства 🙃
Лично мне например важно чтобы в моей системе равенство было разрешимым.
Для "полноты вывода типов" нужно задать
1. полностью аннотированный "core calculus"
2. "surface syntax" в котором аннотировано не всё (и вообще может быть больше конструкций)
3. алгоритм элаборации из второго в первый
Тогда "полноту вывода типов" можно хотя бы сформулировать.
Хотя и этого недостаточно для осмысленных утверждений. Так получится только "масло масляное", потому что типизация алгоритма и так гарантирует, что он строит что-то типизированное.
Был набросок, но после недочётов на которые мне указали в чате, я решил переосмыслить то как мне формализовать своё детище. Поэтому я начал новую итерацию с учётом недочётов.
Да уш, почему-то когда строишь правила вывода «на бумаге» возникает эпично меньше вопросов чем когда делаешь вроде бы тоже самое в прувере🤯
Почему-то в прувере я вижу большинство недочётов в своих построениях ещё до того как он начинает меня бить по рукам. А «на бумаге» я и этих недочётов не вижу и кучу других 🤪
Но тем интереснее и в каком-то смысле проще😋