initial set-up with Lambda as a sub-directory.

Author: Barry-Jay

#script#

@@ -0,0 +1,99 @@
+(* 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 General.v; 
+coqc Test.v;    
+coqc LamSF_Terms.v;
+coqc LamSF_Tactics.v 
+coqc LamSF_Substitution_term.v; 
+
+coqc Beta_Reduction.v;
+coqc LamSF_Redexes.v;
+coqc LamSF_Substitution.v;
+coqc LamSF_Residuals.v;
+coqc LamSF_Marks.v;
+coqc LamSF_Simulation.v;
+coqc LamSF_Cube.v;
+coqc LamSF_Confluence.v;
+
+coqc SF_reduction.v; 
+coqc LamSF_reduction.v; 
+
+coqc LamSF_Normal.v;  
+coqc LamSF_Closed.v;  
+coqc LamSF_Eval.v;   
+coqc Equal.v; 
+coqc Eta;
+ 
+coqc Homomorphism; 
+
+coqc Combinators.v;
+coqc Extensional_to_combinator.v
+coqc Binding.v;
+coqc Unstar
+coqc Intensional_to_combinator.v
+
+
+
+
+