1 (*********************************************************************************************************************************)
2 (* ProgrammingLanguage *)
4 (* Basic assumptions about programming languages . *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import Categories_ch1_3.
12 Require Import InitialTerminal_ch2_2.
13 Require Import Functors_ch1_4.
14 Require Import Isomorphisms_ch1_5.
15 Require Import ProductCategories_ch1_6_1.
16 Require Import OppositeCategories_ch1_6_2.
17 Require Import Enrichment_ch2_8.
18 Require Import Subcategories_ch7_1.
19 Require Import NaturalTransformations_ch7_4.
20 Require Import NaturalIsomorphisms_ch7_5.
21 Require Import MonoidalCategories_ch7_8.
22 Require Import Coherence_ch7_8.
23 Require Import Enrichment_ch2_8.
24 Require Import RepresentableStructure_ch7_2.
25 Require Import FunctorCategories_ch7_7.
27 Require Import NaturalDeduction.
28 Require Import NaturalDeductionCategory.
30 Require Import FreydCategories.
32 Require Import Reification.
33 Require Import GeneralizedArrow.
34 Require Import GeneralizedArrowFromReification.
35 Require Import ReificationFromGeneralizedArrow.
38 * Everything in the rest of this section is just groundwork meant to
39 * build up to the definition of the ProgrammingLanguage class, which
40 * appears at the end of the section. References to "the instance"
41 * mean instances of that class. Think of this section as being one
42 * big Class { ... } definition, except that we declare most of the
43 * stuff outside the curly brackets in order to take advantage of
44 * Coq's section mechanism.
46 Section Programming_Language.
48 Context {T : Type}. (* types of the language *)
50 Context (Judg : Type).
51 Context (sequent : Tree ??T -> Tree ??T -> Judg).
52 Notation "cs |= ss" := (sequent cs ss) : al_scope.
53 (* Because of term irrelevance we need only store the *erased* (def
54 * 4.4) trees; for this reason there is no Coq type directly
55 * corresponding to productions $e$ and $x$ of 4.1.1, and TreeOT can
56 * be used for productions $\Gamma$ and $\Sigma$ *)
58 (* to do: sequent calculus equals natural deduction over sequents, theorem equals sequent with null antecedent, *)
60 Context {Rule : Tree ??Judg -> Tree ??Judg -> Type}.
62 Notation "H /⋯⋯/ C" := (ND Rule H C) : al_scope.
70 * Note that from this abstract interface, the terms (expressions)
71 * in the proof are not accessible at all; they don't need to be --
72 * so long as we have access to the equivalence relation upon
73 * proof-conclusions. Moreover, hiding the expressions actually
74 * makes the encoding in CiC work out easier for two reasons:
76 * 1. Because the denotation function is provided a proof rather
77 * than a term, it is a total function (the denotation function is
78 * often undefined for ill-typed terms).
80 * 2. We can define arr_composition of proofs without having to know how
81 * to compose expressions. The latter task is left up to the client
82 * function which extracts an expression from a completed proof.
84 * This also means that we don't need an explicit proof obligation for 4.1.2.
86 Class ProgrammingLanguage :=
87 { al_eqv : @ND_Relation Judg Rule where "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2)
88 ; al_tsr : TreeStructuralRules
90 ; al_sequent_join : SequentJoin
92 Notation "pf1 === pf2" := (@ndr_eqv _ _ al_eqv _ _ pf1 pf2) : temporary_scope3.
94 Section LanguageCategory.
96 Context (PL:ProgrammingLanguage).
98 (* category of judgments in a fixed type/coercion context *)
99 Definition Judgments_cartesian := @Judgments_Category_CartesianCat _ Rule al_eqv.
101 Definition JudgmentsL := Judgments_cartesian.
103 Definition identityProof t : [] ~~{JudgmentsL}~~> [t |= t].
106 apply al_reflexive_seq.
109 Definition cutProof a b c : [a |= b],,[b |= c] ~~{JudgmentsL}~~> [a |= c].
114 Definition TypesL : ECategory JudgmentsL (Tree ??T) (fun x y => [x|=y]).
116 {| eid := identityProof
119 apply MonoidalCat_all_central.
120 apply MonoidalCat_all_central.
121 unfold identityProof; unfold cutProof; simpl.
122 apply al_subst_left_identity.
123 unfold identityProof; unfold cutProof; simpl.
124 apply al_subst_right_identity.
125 unfold identityProof; unfold cutProof; simpl.
126 apply al_subst_associativity'.
129 Definition Types_first c : EFunctor TypesL TypesL (fun x => x,,c ).
131 eapply Build_EFunctor; intros.
132 eapply MonoidalCat_all_central.
139 Definition Types_second c : EFunctor TypesL TypesL (fun x => c,,x ).
143 Definition Types_binoidal : BinoidalCat TypesL (@T_Branch _).
145 {| bin_first := Types_first
146 ; bin_second := Types_second
150 Definition TypesL_binoidal : BinoidalCat TypesL (@T_Branch _).
154 Definition Types_PreMonoidal : PreMonoidalCat TypesL_binoidal [].
158 Definition TypesEnrichedInJudgments : Enrichment.
159 refine {| enr_c := TypesL |}.
162 Structure HasProductTypes :=
166 (* need to prove that if we have cartesian tuples we have cartesian contexts *)
167 Definition LanguagesWithProductsAreSMME : HasProductTypes -> SurjectiveMonicMonoidalEnrichment TypesEnrichedInJudgments.
171 End LanguageCategory.
173 Structure ProgrammingLanguageSMME :=
174 { plsmme_pl : ProgrammingLanguage
175 ; plsmme_smme : SurjectiveMonicMonoidalEnrichment (TypesEnrichedInJudgments plsmme_pl)
177 Coercion plsmme_pl : ProgrammingLanguageSMME >-> ProgrammingLanguage.
178 Coercion plsmme_smme : ProgrammingLanguageSMME >-> SurjectiveMonicMonoidalEnrichment.
180 Section ArrowInLanguage.
181 Context (Host:ProgrammingLanguageSMME).
182 Context `(CC:CartesianCat (me_mon Host)).
183 Context `(K:@ECategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) C Kehom).
184 Context `(pmc:PreMonoidalCat K bobj mobj (@one _ _ _ (cartesian_terminal C))).
187 Definition ArrowInProgrammingLanguage :=
188 @FreydCategory _ _ _ _ _ _ (@car_mn _ _ _ _ _ _ _ CC) _ _ _ _ pmc.
192 Section GArrowInLanguage.
193 Context (Guest:ProgrammingLanguageSMME).
194 Context (Host :ProgrammingLanguageSMME).
195 Definition GeneralizedArrowInLanguage := GeneralizedArrow Guest Host.
198 Definition ArrowsAreGeneralizedArrows : ArrowInProgrammingLanguage -> GeneralizedArrowInLanguage.
200 Definition TwoLevelLanguage := Reification Guest Host (me_i Host).
202 Context (GuestHost:TwoLevelLanguage).
204 Definition FlatObject (x:TypesL Host) :=
205 forall y1 y2, not ((reification_r_obj GuestHost y1 y2)=x).
207 Definition FlatSubCategory := FullSubcategory (TypesL Host) FlatObject.
211 Context (F:Retraction (TypesL Host) FlatSubCategory).
212 Definition FlatteningOfReification := garrow_from_reification Guest Host GuestHost >>>> F.
213 Lemma FlatteningIsNotDestructive :
214 FlatteningOfReification >>>> retraction_retraction F >>>> RepresentableFunctor _ (me_i Host) ~~~~ GuestHost.
220 End GArrowInLanguage.
222 Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
223 | NLevelLanguage_zero : forall lang, NLevelLanguage O lang
224 | NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n,
225 TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
227 Definition OmegaLevelLanguage : Type :=
228 { f : nat -> ProgrammingLanguageSMME
229 & forall n, TwoLevelLanguage (f n) (f (S n)) }.
231 Close Scope temporary_scope3.
232 Close Scope al_scope.
233 Close Scope nd_scope.
234 Close Scope pf_scope.
236 End Programming_Language.
238 Implicit Arguments ND [ Judgment ].