Existe-t-il un algorithme général pour remplir les trous en termes de calcul des constructions?

Supposons que vous étendez le calcul des constructions avec des "trous" - c'est-à-dire des morceaux de code incomplets que vous n'avez pas encore remplis. Je me demande s'il existe un algorithme pour remplir ces rôles automatiquement. Par exemple (en utilisant la syntaxe de Morte ):

Cas A:

λ (pred : ?) 
-> λ (Nat : *) 
-> λ (Succ : Nat -> Nat) 
-> λ (Zero : Nat)
-> (Succ (pred Nat Succ Zero))

Sur cette situation, un algorithme d'inférence de type peut identifier qui ne ?peut évidemment être ∀ (Nat : *) -> (Nat -> Nat) -> Nat -> Nat, parce que predreçoit Nat : *, Succ : Nat -> Nat, Zero : Natet doit revenir Nat, parce qu'il est le premier argument de Succ.

Cas B:

(Id ? 4)

Où 4 est codé λ et Idest la fonction d'identité (c.-à ∀ (t:*) -> λ (x:t) -> x-d.). Sur cette situation, «?» Est encore une fois clairement ∀ (N:*) -> (N -> N) -> N -> N, car c'est le type de 4.

Cas C:

(Id (Equals Nat 7 (add 3 ?)) (Refl 7))

Ici, Equalset Reflsont définis d'une manière similaire à Idris. ?ne peut évidemment l'être que 4, mais comment le comprendre? Une façon serait d'utiliser le fait que ? : Nat, et Natc'est un type que nous savons comment énumérer, nous pouvons donc simplement tout essayer Natsjusqu'à ce qu'il vérifie. Cela peut être fait pour tout type énumérable.

Cas D:

(Id (Equal Nat 10 (MulPair ?)) 10)

Ici, ?ne peut être que de type Pair Nat; il n'a que plus d'une réponse valable, cependant: il peut être (Pair 10 1), (Pair 2 5), (Pair 5 2)et (Pair 1 10).

Cas E:

(Id (Equal Nat 7 (Mul 2 ?)) 7)

Ici, il n'y a pas de réponse valable, car il 7n'y a pas de multiple de 2.

Tous ces exemples m'ont fait remarquer que nous pouvons créer un algorithme général qui identifie certains modèles connus et donne une réponse en sélectionnant à la main un algorithme spécifique (inférence de type, force brute, etc.), un peu comme Wolfram Alpha trouve la bonne stratégie pour résoudre un intégral. Mais cela ressemble à une approche d'ingénierie / codée en dur. Existe-t-il un moyen de principe de résoudre ce problème? Y a-t-il une étude / un domaine de recherche à ce sujet?

Il y a certainement beaucoup de recherches sur ce problème! Il porte souvent le nom d' élaboration . C'est un problème indécidable en général, comme vous l'avez peut-être deviné. Les "trous" sont souvent appelés méta-variables ou variables d'unification .

Comme je l'explique un peu dans cette réponse , le problème se réduit à une unification d'ordre supérieur , sur laquelle plusieurs personnes ont rédigé des thèses de doctorat entières.

Comme vous le notez dans vos exemples, certains cas sont quelque peu faciles et peuvent être résolus par l'application de règles simples, tandis que certains semblent beaucoup plus difficiles et ont plus une sensation de "théorème prouvant".

Un troisième cas possible est un problème de type "classe de type", où ?représente une sorte de structure , telle qu'une structure de groupe ou de champ, comme dans

mul ? 2 3

avec mul : forall G:Group, G.carrier -> G.carrier -> G.carrierou une variante. Ici, nous devons trouver un Gtel que G.carrier == nat.

En général, vous voulez avoir 3 "régimes" différents pour chaque type de problème, l'unification simple, la démonstration du théorème et les problèmes de résolution de classe respectivement.

Nous l'expliquons un peu dans l'article suivant:

Elaboration in Dependent Type Theory , de Moura, Avigad, Kong & Roux.

Vous voudrez peut-être consulter les références de ce document pour plus d'informations.

J'ai le ventre fort, voici l'open source pour l'élaboration en Lean.

Voici un article wiki qui décrit l' interface avec le concepteur dans Idris.