Per

TL;DR Фірмовий синтаксис Групоїд Інфініті для Mini-TT/Rust MLTT ядра в нормальній формі Бакуса-Наура для LR(1) парсер генераторів загалом, і Menhir/OCaml та LALRPOP/Rust зокрема.

CoC-88

Name: String = { r"[a-zA-Z_][a-zA-Z_\d]*" => <>.to_string() }; Variable: Per = { <n:Name> => Per::Var(n), }; Universe: Per = { <n:r"\*[\d]+"> => Per::Type(u32::from_str_radix(&n[1..],10).unwrap()), <n:r"\*"> => Per::Type(0), }; Lambda: Henk = { "(" <v:Name> ":" <t:Expr> ")" <e:Expr1> => Henk::Lambda(v,Box::new(t),Box::new(e)) }; Forall: Henk = { "[" <v:Name> ":" <t:Expr> "]" <e:Expr1> => Henk::Forall(v,Box::new(t),Box::new(e)) }; // LR(1) Parsing Scheme Expr1: Henk = { Lambda, Forall, Expr2 }; Expr2: Henk = { <l:Expr2> <r:Expr3> => Henk::App(Box::new(l),Box::new(r)), Expr3 }; Expr3: Henk = { Variable, Universe, <l:"("> <e:Expr1> <r:")"> => e }; pub Expr: Henk = { Expr1 };

MLTT-72

Name: String = { r"[a-zA-Z_][a-zA-Z_\d]*" => <>.to_string() }; Variable: Per = { <n:Name> => Per::Var(n), }; Universe: Per = { <n:r"\*[\d]+"> => Per::Type(u32::from_str_radix(&n[1..],10).unwrap()), <n:r"\*"> => Per::Type(0), }; Vars: Vec<Pattern> = { <n:Name> => vec![Pattern::Var(n)], <n:Name> <v:Vars> => { let mut r = v.clone(); r.append(&mut vec![Pattern::Var(n)]); r }, }; Telescope: Vec<(Pattern,Expression)> = { "(" <v:Vars> <m:":"> <t:Expr> ")" => vec![(v[0].clone(),t)], "(" <v:Vars> <m:":"> <t:Expr> ")" <x:Telescope> => { let mut r = x.clone(); r.append(&mut vec![(v[0].clone(),t)]); r } }; Lambda: Per = { "λ" "(" <v:Vars> <m:":"> <t:Expr> ")" <c:","> <e:Exp1> => Per::Lambda(v[0].clone(),None,Box::new(e)), }; Forall: Per = { "Π" "(" <v:Vars> <m:":"> <t:Expr> ")" <c:","> <e:Exp1> => Per::Pi(Typed::new(v[0].clone(),t), Box::new(e)), }; Sigma: Per = { "Σ" "(" <v:Vars> <m:":"> <t:Expr> ")" <c:","> <e:Exp1> => Per::Sigma(Typed::new(v[0].clone(),t), Box::new(e)), }; Exp1: Per = { Lambda, Forall, Sigma, Exp2 }; Exp2: Per = { <l:Exp2> <r:Exp3> => Per::Application(Box::new(l),Box::new(r)), Exp3 }; Exp3: Per = { Universe, Variable, <l:"("> <e:Exp4> <r:")"> => e, }; Exp4: Per = { <l:Exp1> "," <r:Exp4> => Per::Pair(Box::new(l),Box::new(r)), Exp1 }; pub Expr: Per = { Exp1 };

Еволюція синтаксису

Основні лямбла синтаксиси описані були тут.

// ULC = V | ( V : ULC ) ULC | ULC ULC | ( ULC ) -- λ // AUT = V | ( V : AUT ) AUT | AUT AUT | ( AUT ) -- λ // | U | [ V : AUT ] AUT -- Π // PER = V | ( V : PER ) PER | PER PER | ( PER ) -- λ // | U | [ V : PER ] PER | -- Π // | { V : PER } PER | PER , PER | PER .1 | PER .2 -- Σ

ULC — це синтаксис нетипизованого лямбда-числення. AUT — це синтаксис одночасно і мови з однією аксіомою AUTOMATH Ніколаса де Брьойна 1968 року, а пізніше і синтаксис для Calculus of Construction Жерара Юе і його учня Тері Кокана 1988 року, а PER — це MLTT синтаксис для ΠΣ-мови Пера Мартіна-Льофа 1972 року.

Для тих, хто вивчає теорію типів, вправи з написання Π-прувера і ΠΣ-прувера є обов'язковими. Просто Агдою навчитися гратися замало.

Ці синаксис представлені у загальній формі, таку форму зазвичай промислові парсер генератори не приймають, а тільки на комбінаторах чи PEG парсерах. Промислові парсер-генератори приймають БНФ граматики написані у LL(1), LR(1), LALR(1) та інших більш strict формах. Найстарійша і найпопулярніша форма LR(1), яка заглядає на один токен вправо і вліво була вибрана як основа для синтаксисів вищих мов Групоїд Інфініті. За основу лямбда сиснтаксиса була взята мова Lean від Microsoft.

Мій учень попросив мене специфікувати ці синтаксис і зробити максимально зрозумілими для Rust програмістів, тому ми взяли LALRPOP, який є канонічним LR(1) парсер-генератором і написали на ньому спочатку CoC-88, а потім MLTT-72.

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

Чому ці вправи важливі? Тому, що лямбда числення вищих порядків є внутрішньою мовою локальних декартово-замкнених категорій, і як кажуть поза очі головні дослідники області є природньою формою мислення. За тисячі років людської думки ми не придумали до цих пір більш зручних логік які б не вбудовувалися в цей тайпчекер, більше того, всі мови всіх математик теж зводяться до "для всіх x: A, виконується предикат P(x)" і "існує таке x: A, що виконується предикат P(x)", перше Π або ∀, друге Σ або Ǝ.

Проблеми Гьоделівської нескінченності і обмеження першої теореми про неповноту стосується по-перше систем першого порядку, по-друге аплікейбл до обмеженої кількості аксіом. Предикативні математичні тайпчекери вищих порядків мають нескінченну кількість всесвітів навіть для одного типу, тому теж можуть містити метациркулярні доведення і гомотопічні транспорти одних візерунків в інші, власне вся магія відбувається при доведенні цих ізоморфізмів.

Фінальною точкою, коли людська думка змогла формалізувати мову математики у повному обсязі, не залишивши поза собою жодної теореми, яку не можна було би верифікувати механістично, став 2017 рік з виходом експериментального тайпчекера cubicaltt, який пізніше влився в Agda 2.6 і з тих пір є головним обчислювальним ядром, основного гомотопічного прувера планети.

Існує тільки три інституції в світі які утримують кубічну думку і розуміння як влаштовані ці тайпчекери:

1) Університет Карнегі-Меллона, Піттсбург, США — 🇺🇸 ;
2) Технічний університет Чалмерса, Гетеборг, Швеція — 🇸🇪 ;
3) Політехніка Сікорського, Київ, Україна — 🇺🇦 .

Відповідь на питання чому саме така конструкція є нормальною формою мислення дається в курсі алгебраїчної топології, теорії розшарувань, та в 2.3 параграфі підручнику HoTT. Також Сергій Максименко з НАН України давав публічну вступну лекцію на цю тему.

Я назавжди залишуся людиною, яка принесла гомотопічну теорію типів в Україну і побудувала свою школу і свою лінію виробництва артефіктів (лабораторію).