-
Notifications
You must be signed in to change notification settings - Fork 0
/
README
98 lines (72 loc) · 4.23 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
(*****************************************************************************)
(* Projet Coq - Calculus of Inductive Constructions V5.10 *)
(*****************************************************************************)
(* *)
(* Meta-theory of the explicit substitution calculus lambda-env *)
(* Amokrane Saibi *)
(* *)
(* September 1993 *)
(* *)
(* Revised version : December 1994 *)
(* *)
(*****************************************************************************)
Le principal re'sultat de ce de'veloppement est la confluence du
lambda-sigma-lift-calcul (appele' aussi lambda-env-calcul). Ce syste`me
de re'e'criture a e'te' de'fini par T. Hardin et J.-J. Le'vy.
Fichier a` charger: confluence_LSL.v
Description des fichiers:
=========================
* Re'sultats ge'ne'raux:
----------------------
- sur_les_relations.v : de'finitions ge'ne'rales concernant les
relations, confluence, noethe'rianite'...
- Newman.v : lemme de Newman.
- Yokouchi.v : lemme de Yokouchi.
* La the'orie:
------------
- TS.v : de'finition de l'alge`bre: termes et
substitutions explicites.
- sigma_lift.v : de'finition d'un sous-syste`me du
lambda-sigma-lift-calcul, appelle'
sigma-lift (ou SL).
- lambda_sigma_lift.v : de'finition du lambda-sigma-lift-calcul
(ou LSL).
- egaliteTS.v : l'e'galite' dans l'alge`bre.
* Etapes de la preuve:
--------------------
** noethe'rianite' de sigma-lift:
------------------------------
- comparith.v : comple'ments d'arithme'tique, utilse
les re'sultats de ARITH.
- Pol1.v : polynome P1.
- Pol2.v : polynome P2.
- terminaison_SL.v : sigma-lift est noetherien en utilisant
un ordre lexicographique combine avec une
interpretation polynomiale par P1 et P2.
** confluence locale de sigma-lift:
--------------------------------
- inversionSL.v : inversion de la relation sigma-lift.
- determinePC_SL.v : determination des paires critiques de sigma-lift.
- resoudPC_SL.v : resolution des paires critiques de sigma-lift.
- conf_local_SL.v : confluence locale de sigma-lift.
** confluence forte de Beta||:
---------------------------
- betapar.v : de'finition de la parallelisation de la
regle Beta: beta_par (ou B||).
- conf_strong_betapar.v : confluence forte de beta_par.
** re'sultat technique:
--------------------
- SLstar_bpar_SLstar.v : de'finition de "SL* o B|| o SL*".
- commutation.v : le diagramme si-dessous commute:
B||
x ---------> z
| |
SL | |SL*
| |
V V
y ----------> u
SL*B||SL*
** confluence du lambda-sigma-lift-calcul:
---------------------------------------
- confluence_LSL.v : confluence du lambda-sigma-lift-calcul
en utilisant tous les re'sultats ci-dessus.