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

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 $CC^{bi}$$CC$ au lieu de ( i $(id\; 0)$ . Si nous supposons un système de définitions globales, alors,$(id\; \mathbb{N}\; 0)$

$id : (\Pi A\; |\; \mathsf{Type}\; . (\Pi x : A\; . A))$

et

.$id = (\lambda A\; |\; \mathsf{Type}\; . (\lambda 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 ?$(id\; 0)$$CC^{bi}$

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?$CC^{bi}$

Edit: Pour être plus précis, je demande comment est accepté à la place de ( i $(id\; 0)$ 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.$(id\; \mathbb{N}\; 0)$$\Pi$$:$$|$

$\Pi$

$(id\; 0)$$(id\; \mathbb{N}\; 0)$

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=\lambda x. x$