Questions marquées «dependent-type»

Je suis intéressé à obtenir une compréhension vraiment solide sur la dactylographie dépendante. J'ai lu la majeure partie de TaPL et lu (s'il n'est pas complètement assimilé ) "Types dépendants" dans ATTaPL . J'ai également lu et parcouru de nombreux articles sur la dactylographie dépendante. De...

Coq a le type Prop de preuve des propositions non pertinentes qui sont rejetées lors de l'extraction. Quelle est la raison de cela si nous utilisons Coq uniquement pour les preuves. Prop est imprédicatif, donc Prop: Prop, cependant, Coq déduit automatiquement les index d'univers et nous pouvons...

J'ai lu des articles sur les types dépendants et les contrats de programmation. D'après la majorité de ce que j'ai lu, il semble que les contrats soient des contraintes vérifiées dynamiquement et que les types dépendants soient vérifiés statiquement. Certains documents m'ont fait penser qu'il était...

Quelqu'un pourrait-il expliquer la différence entre: Types de données algébriques (que je connais assez bien) Types de données algébriques généralisés (qu'est-ce qui les rend généralisés?) Types inductifs (par exemple Coq) (Types particulièrement inductifs.)

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 {} {∅ ⊢ * : ◽}...

Imaginez, nous avons défini les nombres naturels dans le calcul lambda typé de manière dépendante comme des chiffres de l'Église. Ils peuvent être définis de la manière suivante: SimpleNat = (R : Set) → R → (R → R) → R zero : SimpleNat zero = λ R z _ → z suc : SimpleNat → SimpleNat suc sn = λ R z s...

Il est bien connu que dans le système F, vous pouvez coder des produits binaires avec le type Vous pouvez alors définir des fonctions de projection de pi_1 de: A \ fois B \ to A et \ pi_2: Temps A \ B \ B .π 1 : A × B → A π 2 : A × B → BA × B ≜ ∀ α .( A → B → α ) → αUNE×B≜∀α.(UNE→B→α)→α A \times B...

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...

Dans le chapitre 1 et l'annexe A du livre Hott , plusieurs familles de types primitifs sont présentées (types d'univers, types de fonctions dépendantes, types de paires dépendantes, types de coproduits, type vide, type d'unité, type de nombre naturel et types d'identité) pour former la base pour la...

Je m'intéresse à la modélisation d'objets, de la programmation orientée objet, à la théorie des types dépendants. Comme application possible, j'aimerais avoir un modèle où je peux décrire différentes fonctionnalités des langages de programmation impératifs. Je n'ai pu trouver qu'un seul article sur...

Est-il vrai que l'ajout d'axiomes au CIC pourrait avoir des influences négatives sur le contenu informatique des définitions et des théorèmes? Je comprends que, dans le comportement normal, un terme fermé réduit à sa forme normale canonique de la théorie, par exemple , si est vrai, alors n doit...

Il est bien connu que la propriété Church-Rosser est valable pour réduction de β η dans le calcul lambda simplement typé. Cela implique que le calcul est cohérent, en ce sens que toutes les équations impliquant des termes λ ne sont pas dérivables: par exemple, K ≠ I , car elles ne partagent pas la...

J'ai appris quelque chose sur l'implémentation de types dépendants, comme ce tutoriel , mais la plupart d'entre eux implémentent des interprètes. Ma question est, il semble que l'implémentation d'un compilateur pour le type dépendant soit beaucoup plus difficile qu'un compilateur, car vous pouvez...

J'expérimente des systèmes de type pur dans le cube lambda de Barendregt, en particulier avec le plus puissant, le Calcul des constructions. Ce système a des sortes *et BOX. Pour mémoire, j'utilise ci-dessous la syntaxe concrète de l' Morteoutil https://github.com/Gabriel439/Haskell-Morte-Library...

Je me demande si quelqu'un peut me donner l'intuition derrière pourquoi la positivité stricte des types de données inductifs garantit une forte normalisation. Pour être clair, je vois comment avoir des occurrences négatives conduit à la divergence, c'est-à-dire en définissant: data X where Intro :...

Je suis dans une situation où je dois montrer que la vérification de typage est décidable pour un calcul typé de manière dépendante sur lequel je travaille. Jusqu'à présent, j'ai pu prouver que le système est en train de normaliser fortement, et donc que l'égalité définitionnelle est décidable....

C'est un fait assez bien connu que dériver une contradiction d'une inégalité (par exemple, ) dans la théorie de type Martin-Loef nécessite un univers.(0=1)→⊥(0=1)→⊥(0=1) \to \bot La preuve est également assez simple - en l'absence d'univers, nous pouvons effacer les dépendances de tout type...

Disons que je travaille dans la théorie des types d'homotopie et que mes seuls objets d'étude sont des catégories conventionnelles. Equivalences ici sont donnés par foncteurs et G : C ⟶ D qui fournissent des équivalences de catégories C ≃ D . Il existe des isomorphismes naturels α : n a t ( F G , 1...

La plupart des assistants de preuve ont formalisé le concept de "jeu fini". Ces formalisations diffèrent cependant énormément (même si l'on espère qu'elles sont toutes essentiellement équivalentes!). Ce que je ne comprends pas à ce stade, c'est l'espace de conception impliqué et quels sont les...

Je me demandais si l'ordre des déclarations de type inductif pouvait avoir de l'importance. Par exemple, dans Coq, vous pouvez définir Natsoit par: Inductive Nat := | O : Nat | S : Nat -> Nat. ou Inductive Nat := | S : Nat -> Nat | O : Nat. Cela changera peut-être l'ordre des paramètres dans...