Quel est le rôle du calcul bicolore des constructions?

9

Donc, je lis un peu sur l'élaboration, en particulier, les algorithmes basés sur le calcul bicolore de la construction, et je suis un peu confus. Je ne comprends pas exactement à quoi sert le . Il semble être identique à C C sauf qu'il existe une distinction entre les arguments implicites et explicites pour les fonctions. En particulier, je ne vois pas comment cela vous permet d'écrire ( i dCCbiCC au lieu de ( i d(id0) . Si nous supposons un système de définitions globales, alors,(idN0)

id:(ΠA|Type.(Πx:A.A))

et

.id=(λA|Type.(λx:A.x))

Les règles permettent-elles vraiment ? Bien sûr, la syntaxe le fait, mais je ne le vois pas dans la relation de frappe. Suis-je en train de manquer quelque chose? Suis-je en train demalcomprendre le rôle de C C b i ?(id0)CCbi

De plus, la propriété de confluence n'est-elle pas perdue? Je suppose que mon problème est que je lis sur l'élaboration sans avoir beaucoup lu sur avant cela. Qu'est-ce qu'un bon article qui le présente et seul?CCbi

Edit: Pour être plus précis, je demande comment est accepté à la place de ( i d(id0) lorsque les règles explicites et implicites Π application sont identiques modulo sytnax. Je ne vois aucune différence entre : et | les règles pour les deux semblent les mêmes.(idN0)Π:|

Π

(id0)(idN0)

Anthony
la source
2
Comme je l'ai dit ci-dessous, votre intuition est correcte: le calcul bicolore des constructions est un calcul explicite, dans lequel les arguments omis par l'utilisateur mais élaborés par le "front end" sont explicitement marqués. En outre, la confluence est perdue pour les réductions bêta + eta, mais elle est vraie si elle est limitée à la seule version bêta.
cody

Réponses:

9

Dans Le calcul implicite des constructions étendant les systèmes de type pur avec un liant de type intersection et le sous-typage , Alexandre Miquel présente les concepts de base pour le calcul implicite des constructions, qui je pense est synonyme du calcul bicolore des constructions.

Le but est (entre autres) d'avoir un calcul sans l'encombrement d'annotations de type explicites partout. L'inférence de type est cependant (très probablement) indécidable.

id=λx.x

id:X:Type.XX
id:NatNat
id 0:Nat
Le système admet la réduction et la confluence du sujet, même sur des termes non typés (ce qui en fait échoue pour les calculs avec des annotations d'abstraction). Tout cela se retrouve dans la thèse d'Alexandre, malheureusement en français. Je ne suis pas sûr d'avoir une meilleure référence pour ces résultats, bien que j'en ai peur.
cody
la source
Je connaissais la première partie de votre réponse, mais je pense que j'aurais dû être plus précis dans ma question initiale. C'est-à-dire, comment exactement (id 0) est-il autorisé si id a le type (\ Pi X | Type. X -> X) car il semble que la règle APP soit identique pour les \ Pi implicites et explicites. Dans le calcul implicite des constructions, qui est en fait une théorie différente, ce n'est pas le cas car il est séparé en APP et GEN. Pour vérifier qu'il est différent, vérifiez la rubrique "Un calcul avec des arguments" vraiment implicites "" dans le document que vous avez référencé.
Anthony
1
Concernant la décidabilité. Le document auquel vous faites référence suppose que sa théorie est indécidable. Le document auquel il fait référence (je suppose que le calcul bicolore "original" du papier de construction) prétend être décidable mais ne le prouve pas explicitement. Je l'ai lu après avoir posté cette question et il semble qu'elle devrait certainement être décidable et, selon les restrictions syntaxiques, conserver la confluence. D'un autre côté, je suis toujours coincé avec ma confusion d'origine: \
Anthony
Vous devriez peut-être nous dire quel document vous regardez.
cody
2
Ok, j'ai jeté un œil à Elaboration and Erasure in Type Theory de Marko Luther, qui, je suppose, est votre référence. Dans ce cas, il n'y a pas de différence sémantique entre les produits explicites et implicites, et en effet le système bicolore est une extension conservatrice du calcul des constructions. Ce qui se passe, c'est que vous utilisez l' élaboration pour prendre un terme sans l'argument explicite pour le transformer en un terme entièrement annoté: id !1 0élabore à id Nat 0. Dans ce texte, l'élaboration est traitée dans la section 4.
cody
CCbi