-
Notifications
You must be signed in to change notification settings - Fork 3
/
script
99 lines (78 loc) · 4.33 KB
/
script
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
(* This program is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1 *)
(* of the License, or (at your option) any later version. *)
(* *)
(* This program is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this program; if not, write to the Free *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA *)
(**********************************************************************)
(* Intensional Lambda Calculus *)
(* *)
(* is implemented in Coq by adapting the implementation of *)
(* Lambda Calculus from Project Coq *)
(* 2015 *)
(**********************************************************************)
(**********************************************************************)
(* script *)
(* *)
(* Barry Jay *)
(* *)
(**********************************************************************)
(*
The files for building the Lambda-Factor Calculus, and proving some useful properties.
Many files are adapted from Lambda Calculus in Project Coq. The new files are
coqc General.v; (* various things *)
coqc Lambda_tactics.v (* some tactics *)
coqc Substitution_term.v; (* a variation on Substitution.v *)
coqc SF_reduction.v; (* operator reductions *)
coqc LamSF_reduction.v; (* all reductions *)
coqc Normal.v; (* normal forms *)
coqc Closed.v; (* closed terms *)
coqc Eval.v; (* evaluation tactics *)
coqc Equal.v; (* decidable equality of closed normal forms *)
coqc Combinators (* decide if a program is a combinator *)
coqc Analysis.v; (* conversion of closed normal forms to combinators and back *)
The main theorems are:
1. lambda-factor calculus is a conservative extension of pure lambda calculus
2. lambda-factor calculus is a conservative extension of SF-calculus.
3. lambda-factor calculus is confluent.
4. The irreducible terms are easily characterised (as the normal forms).
5. equality of closed normal forms is definable.
6. closed normal forms can be converted to combinators having the same extensional behaviour
by application of a term, concrete.
7. concrete also preserves intensional behaviour (i.e. no infomration loss)
since it can be reversed by application of another term, abstract.
*)
coqc -Q Lambda Lambda General.v;
coqc -Q Lambda Lambda Test.v;
coqc -Q Lambda Lambda LamSF_Terms.v;
coqc -Q Lambda Lambda LamSF_Tactics.v
coqc -Q Lambda Lambda LamSF_Substitution_term.v;
coqc -Q Lambda Lambda Beta_Reduction.v;
coqc -Q Lambda Lambda LamSF_Redexes.v;
coqc -Q Lambda Lambda LamSF_Substitution.v;
coqc -Q Lambda Lambda LamSF_Residuals.v;
coqc -Q Lambda Lambda LamSF_Marks.v;
coqc -Q Lambda Lambda LamSF_Simulation.v;
coqc -Q Lambda Lambda LamSF_Cube.v;
coqc -Q Lambda Lambda LamSF_Confluence.v;
coqc -Q Lambda Lambda SF_reduction.v;
coqc -Q Lambda Lambda LamSF_reduction.v;
coqc -Q Lambda Lambda LamSF_Normal.v;
coqc -Q Lambda Lambda LamSF_Closed.v;
coqc -Q Lambda Lambda LamSF_Eval.v;
coqc -Q Lambda Lambda Equal.v;
coqc -Q Lambda Lambda Eta;
coqc -Q Lambda Lambda Homomorphism;
coqc -Q Lambda Lambda Combinators.v;
coqc -Q Lambda Lambda Extensional_to_combinator.v
coqc -Q Lambda Lambda Binding.v;
coqc -Q Lambda Lambda Unstar
coqc -Q Lambda Lambda Intensional_to_combinator.v