Le CoC serait le point culminant des trois dimensions du Lambda Cube. Cela ne m’apparaît pas du tout. Je pense que je comprends les dimensions individuelles, et la combinaison de deux semble entraîner une union relativement simple (peut-être que je manque quelque chose?). Mais quand je regarde le...
Coq, Agda et Idris ont une hiérarchie de types infinie (Type 1: Type 2: Type 3: ...). Mais pourquoi ne pas le faire à la place comme λC, le système du cube lambda le plus proche du calcul des constructions, qui n'a que deux sortes, et ◽ , et ces règles?∗∗*◽◽◽ ∅⊢∗:◽∅⊢∗:◽\frac {} {∅ ⊢ * : ◽}...
Pour les systèmes sans types dépendants, comme le système de type Hindley-Milner, les types correspondent à des formules de logique intuitionniste. Là, nous savons que ses modèles sont des algèbres de Heyting, et en particulier, pour réfuter une formule, nous pouvons nous limiter à une algèbre de...
La théorie du type de Martin-Löf est-elle fondamentalement le calcul prédicatif des constructions inductives sans imprédicatif ?PropProp\mathtt{Prop} S'ils sont étroitement liés mais avec plus de différences que simplement , quelles sont ces
Je suis conscient que le calcul des constructions est en train de normaliser fortement, ce qui signifie que chaque expression a une normale pour laquelle elle ne peut pas être bêta, eta-réduite davantage. Il s'agit donc en fait de l'expression la plus efficace qui calcule la même valeur que...
Dans le papier classique du calcul des constructions , il y a une règle qui dit (page 7 du pdf, page 101 du document original) Cette règle signifierait que tout contexte est réductible à un membre de ce contexte. Il semble que cela ne devrait pas être correct, car cela impliquerait 1 ≅ Nat 3 ≅ Nat...
Je veux savoir si la décidabilité de l'égalité de deux preuves décidables de la même proposition peut être prouvée sans aucun axiome supplémentaire dans le Calcul des constructions inductives. Plus précisément, je veux savoir si cela est vrai sans aucun axiome supplémentaire dans Coq....