X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=5ae7da3063e1448a8bed8e391e332259463afc03;hb=ecb63d645415784352a937f8320f84c23da327f7;hp=5cdf1b2ff7b8e27fda97dba3f5a7c07197204b18;hpb=b665b25cc0b62aa5bd7e90224fe7a28d15e122f2;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 5cdf1b2ff..5ae7da306 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -23,7 +23,7 @@
[Spacer]
-
+

@@ -36,18 +36,24 @@ news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - @@ -56,16 +62,20 @@ milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 - - (background - core - applications) - library + (static LDDL directory) @@ -74,30 +84,42 @@ visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 + helena - +
- - helena -
- - -
Summary of the Specification [spacer] + +
Summary of the Specification [spacer]
-
Here is a numerical acount of the specification's contents +
Here is a numerical account of the specification's contents and its timeline.
-
+
@@ -122,80 +144,91 @@ - + - + - + - + - + - + - + - + - +
sizes files358102 characters43183769295 nodes1860162245853
propositions theorems13034 lemmas1286256 total1416290
concepts declared5421 defined8929 total14350
- -
Stage "B"
-
    +
    Stage "B"
    +
    • Ongoing. Context-sensitive subject equivalence for native type assignment.
    - -
    Stage "A": "Extending the Applicability Condition"
    -
      +
      Stage "A2": "Extending the Applicability Condition"
      +
        +
      • + 2015 October 9. + λδ version 2A2 is started. +
        • +
      +
      Stage "A1": "Extending the Applicability Condition"
      +
        +
      • + 2015 August 27. + λδ version 2A1 appears too complex and is dismissed. +
        • +
      +
      • 2014 October 28. - λδ version 2A is released. + λδ version 2A1 is released.
      -
        +
        • 2014 September 9. Iterated static type assignment defined (more elegantly) as a primitive notion.
        -
          +
          • 2014 June 18. Preservation of stratified native validity for context-sensitive computation on terms.
          -
            +
            • 2014 June 9. Strong qrst-normalization for simply typed terms.
            -
              +
              • 2014 April 16. Lazy equivalence on local environments - addded as q-step to rst-computation on closures + added as q-step to rst-computation on closures (anniversary milestone).
              -
                +
                • 2014 January 20. Parametrized slicing of local environments @@ -203,26 +236,26 @@ (one from basic_1, the other used in basic_2 till now).
                -
                  +
                  • 2013 August 7. Passive support for global environments.
                  -
                    +
                    • 2013 July 27. Reaxiomatized β-reductum as in rt-reduction.
                    -
                      +
                      • 2013 July 20. Context-sensitive strong rt-normalization for simply typed terms.
                      -
                        +
                        • 2013 April 16. Reaxiomatized substitution and reduction @@ -230,26 +263,26 @@ (anniversary milestone).
                        -
                          +
                          • 2013 March 16. Mutual recursive preservation of stratified native validity for rst-computation on closures.
                          -
                            +
                            • 2012 October 16. Confluence for context-free parallel reduction on closures.
                            -
                              +
                              • 2012 July 26. Term binders polarized to control ζ-reduction (not released).
                              -
                                +
                                • 2012 April 16. Context-sensitive subject equivalence @@ -257,43 +290,42 @@ (anniversary milestone).
                                -
                                  +
                                  • 2012 March 15. Context-sensitive strong normalization for simply typed terms.
                                  -
                                    +
                                    • 2012 January 27. Support for abstract candidates of reducibility.
                                    -
                                      +
                                      • 2011 September 21. Confluence for context-sensitive parallel reduction on terms.
                                      -
                                        +
                                        • 2011 September 6. Confluence for context-free parallel reduction on terms.
                                        -
                                          +
                                          • 2011 April 17. - Specification starts. + λδ version 2 is started.
                                          - -
                                          Logical Structure of the Specification [spacer] +
                                          Logical Structure of the Specification [spacer]
                                          -
                                          This table reports the specification's components and their planes. +
                                          This table reports the specification's components and their planes.
                                          -
                                          +
                                          @@ -311,518 +343,10 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + @@ -834,9 +358,9 @@ - - - + + + @@ -845,80 +369,42 @@ - - - - - - - - - - - - - - - - - - - - - + + + - - - - - - + + + - - + - - - - - - - - - - @@ -927,138 +413,10 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + @@ -1073,8 +431,8 @@ - - + + @@ -1083,20 +441,12 @@ - + + + - - - - - - - - - - - @@ -1111,10 +461,8 @@ - - + + @@ -1126,9 +474,9 @@ - - - + + + @@ -1140,23 +488,11 @@ - - - - - - - - - - - + + @@ -1168,9 +504,9 @@ - - - + + + @@ -1182,9 +518,9 @@ - - - + + + @@ -1193,40 +529,24 @@ - - - - - + + + + - - - - - - - - - - - - - + + + @@ -1288,7 +608,9 @@ - +
                                          examplesterms with special featuresex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta -
                                          -                                           		-
                                          -                                           		-
                                          -
                                          - - - -
                                          -                                           		-
                                          -                                           		-
                                          -
                                          dynamic typinglocal env. ref. for stratified native validitylsubsv ( ? ⊢ ? ⫃¡[?,?] ? )lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		stratified native validityshnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] ) -
                                          -                                           		-
                                          -                                           		-
                                          -
                                          -
                                          -                                           		-
                                          -                                           		snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_fsb snv_scpes snv_preserve -
                                          -                                           		-
                                          -
                                          equivalencedecomposed rt-equivalencescpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )scpes_aaa scpes_cpcs scpes_scpes -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		context-sensitive equivalencecpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs -
                                          -                                           		-
                                          -
                                          conversioncontext-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc -
                                          -                                           		-
                                          -
                                          computationevaluation for context-sensitive rt-reductioncpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ ) -
                                          -                                           		-
                                          -                                           		-
                                          -
                                          -
                                          -                                           		evaluation for context-sensitive reductioncpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		strongly normalizing qrst-computationfsb ( ⦥[?,?] ⦃?,?,?⦄ )fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )fsb_aaa fsb_csx -
                                          -
                                          -
                                          -                                           		strongly normalizing rt-computationlcosx ( ? ⊢ ~⬊*[?,?,?] ? )lcosx_cpx -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		-
                                          -                                           		lsx ( ? ⊢ ⬊*[?,?,?,?] ? )lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )lsx_drop lsx_lpx lsx_lpxs llsx_csx -
                                          -
                                          -
                                          -                                           		-
                                          -                                           		csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_tsts_vector csx_aaa -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		-
                                          -                                           		csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs -
                                          -
                                          -
                                          -                                           		parallel qrst-computationfpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		-
                                          -                                           		fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs -
                                          -
                                          -
                                          -                                           		decomposed rt-computationscpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )scpds_lift scpds_aaa scpds_scpds -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		context-sensitive rt-computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		-
                                          -                                           		cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tsts cpxs_tsts_vector cpxs_lreq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		context-sensitive computationlprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_drop lprs_cprs lprs_lprs -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		-
                                          -                                           		cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)cprs_lift cprs_cprs -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		local env. ref. for generic reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drop lsubc_drops lsubc_lsuba -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		support for generic computation propertiesgcpgcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )gcp_aaa -
                                          -
                                          reductionparallel qrst-reductionfpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )fpbq_lift fpbq_aaa -
                                          -
                                          -
                                          -                                           		-
                                          -                                           		fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpb_lift fpb_lleq fpb_fleq -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		normal forms for context-sensitive rt-reductioncnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )cnx_lift cnx_crx cnx_cix -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		context-sensitive rt-reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_drop lpx_frees lpx_lleq lpx_aaa -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		-
                                          -                                           		cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		irreducible forms for context-sensitive rt-reductioncix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )cix_lift -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		reducible forms for context-sensitive rt-reductioncrx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )crx_lift -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		normal forms for context-sensitive reductioncnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_drop lpr_lpr -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		-
                                          -                                           		cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_llpx_sn cpr_cir -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		irreducible forms for context-sensitive reductioncir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )cir_lift -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		reducible forms for context-sensitive reductioncrr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )crr_lift -
                                          -                                           		-
                                          -
                                          unfoldunfoldunfold ( ⦃?,?⦄ ⊢ ? ⧫* ? ) -
                                          -                                           		static typingparametersshsd

                                          		iterated static type assignmentlstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstasrestricted ref. for local env.lsubr ( ? ⫃ ? )lsubr_length lsubr_drops lsubr_lsubr
                                          static typinglocal env. ref. for degree assignmentlsubd ( ? ⊢ ? ⫃▪[?,?] ? )lsubd_da lsubd_lsubd -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_aaa da_da -
                                          -                                           		-
                                          -
                                          +
                                          		parametersshsd + ranged equivalence for closuresfreq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )freq_freq
                                          		+
                                          +
                                          		local env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_aaa lsuba_lsuba + context-sensitive free variablesfrees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )frees_weight frees_lreq frees_frees
                                          		+
                                          + s-computation +
                                          		atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa
                                          		-
                                          -
                                          -
                                          -                                           		restricted local env. ref.lsubr ( ? ⫃ ? )lsubr_lsubr
                                          multiple substitutionlazy equivalencefleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )fleq_fleq -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		-
                                          -                                           		lleq ( ? ≡[?,?] ? )lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		lazy pointwise extension of a relationllpx_snllpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_lreq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		pointwise union for local environmentsllor ( ? ⋓[?,?] ? ≡ ? )llor_alt llor_drop -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		context-sensitive exclusion from free variablesfrees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )frees_append frees_lreq frees_lift -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		contxt-sensitive multiple rt-substitutioncpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )cpys_lift cpys_cpys -
                                          -
                                          -
                                          -                                           		iterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_alt fqus_fqus -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		-
                                          -                                           		fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_fqup -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		iterated local env. slicingdrops ( ⬇*[?,?] ? ≡ ? )drops_drop drops_drops -
                                          -                                           		-
                                          -
                                          -
                                          -                                           		generic term relocationlifts_vector ( ⬆*[?] ? ≡ ? )lifts_lift_vectors-transitionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_length fquq_weight

                                          		lifts ( ⬆*[?] ? ≡ ? )lifts_lift lifts_liftsfqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )fqu_length fqu_weight
                                          + relocationgeneric slicing for local environmentsdrops_vector ( ⬇*[?,?] ? ≡ ? )
                                          		support for multiple relocationmr2 ( @⦃?,?⦄ ≡ ? )mr2_plus ( ? + ? )mr2_minus ( ? ▭ ? ≡ ? )mr2_mr2
                                          substitutionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )

                                          		fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) -
                                          -                                           		drops ( ⬇*[?,?] ? ≡ ? )drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops

                                          		global env. slicinggget ( ⬇[?] ? ≡ ? )gget_ggetgeneric relocation for termslifts_vector ( ⬆*[?] ? ≡ ? )lifts_lifts_vector

                                          		contxt-sensitive ordinary rt-substitutioncpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )cpy_lift cpy_nlift cpy_cpy -
                                          -                                           		-
                                          -
                                          +
                                          		local env. ref. for rt-substitutionlsuby ( ? ⊆[?,?] ? )lsuby_lsubylifts ( ⬆*[?] ? ≡ ? )lifts_simple lifts_weight lifts_lifts

                                          		pointwise extension of a relationlpx_snlpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_snranged equivalence for local environmentslreq ( ? ≡[?] ? )lreq_length lreq_lreq

                                          		basic local env. slicingdrop ( ⬇[?,?,?] ? ≡ ? )drop_append drop_lreq drop_dropgeneric entrywise extension of context-sensitive relations for termalexs ( ? ⦻*[?,?,?] ? )lexs_length lexs_lexs
                                          -
                                          -                                           		basic term relocationlift_vector ( ⬆[?,?] ? ≡ ? )lift_lift_vector + grammarappend for local environmentsappend ( ? @@ ? )append_length
                                          		+
                                          -
                                          -                                           		-
                                          -                                           		lift ( ⬆[?,?] ? ≡ ? )lift_neq lift_lift -
                                          -                                           		+
                                          grammarequivalence for local environmentslreq ( ? ⩬[?,?] ? )lreq_lreqcontext-sensitive equivalences for termsceqceq_ceq
                                          		lenv lenv_weight ( ♯{?} ) lenv_length ( |?| )lenv_append ( ? @@ ? ) +
                                          +
                                          @@ -1339,8 +661,7 @@
                                          - -
                                          +
                                          [Spacer]
                                          @@ -1366,6 +687,6 @@

                                          -
                                          Last update: Sat, 01 Nov 2014 17:50:22 +0100
                                          - +
                                          Last update: Fri, 01 Apr 2016 23:30:53 +0200
                                          +