Говорят, что КО является кульминацией всех трех измерений лямбда-куба. Это не очевидно для меня вообще. Я думаю, что я понимаю отдельные измерения, и комбинация любых двух, кажется, приводит к относительно простому объединению (возможно, я что-то упускаю?). Но когда я смотрю на CoC, вместо того,...
Coq, Agda и Idris имеют бесконечную иерархию типов (Тип 1: Тип 2: Тип 3: ...). Но почему бы не сделать это, как λC, систему в лямбда-кубе, которая ближе всего к исчислению конструкций и имеет только два , ∗** и , и эти правила?◽◽◽ ∅⊢∗:◽∅⊢∗:◽\frac {} {∅ ⊢ * : ◽}...
Для систем без зависимых типов, таких как система типов Хиндли-Милнера, типы соответствуют формулам интуиционистской логики. Там мы знаем, что ее модели являются гейтинговыми алгебрами, и, в частности, чтобы опровергнуть формулу, мы можем ограничиться одной гейтинговой алгеброй, где каждая формула...
Является ли теория типов Мартина-Лёфа в основном предикативным исчислением индуктивных конструкций без предиктивного ?П р о пProp\mathtt{Prop} Если они тесно связаны , но с большим количеством различий , чем просто , каковы эти различия?П р о...
Я знаю, что исчисление конструкций сильно нормализуется, то есть у каждого выражения есть норма, которая не может быть бета, далее сокращена. Так что на самом деле это наиболее эффективное выражение, которое вычисляет то же значение, что и исходное выражение. Но в некоторых случаях нормализация...
В классическом исчислении конструкций бумаги есть правило, которое гласит (стр. 7 из pdf, стр. 101 оригинального документа) Это правило будет означать, что любой контекст сводится к члену этого контекста. Кажется, что это не должно быть правильно, так как это повлечет за собой 1 ≅ Nat 3 ≅ Nat 1 ≅ 3...
Я хочу знать, может ли быть доказана разрешимость равенства двух разрешимых доказательств одного и того же предложения без каких-либо дополнительных аксиом в исчислении индуктивных построений. В частности, я хочу знать, правда ли это, без каких-либо дополнительных аксиом в Coq....