[\lambda\delta home]
cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
[Spacer]

home news specification

documentation implementation
foreword milestones version 2 (background - core - applications)
version 2 helena Open Symbolic Notation (OSN)
citations visibility version 1 (background - core) (static HELM directory) version 1 library (static LDDL directory)
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline.
category units




sizes characters (files) 324288 (318) nodes (objects) 1490591 (1484) intrinsic loss factor 4.6
propositions theorems 99 lemmas 1124 total 1223
concepts declared 35 defined 94 total 129
Stage "B"
Stage "A2": "Extending the Applicability Condition"
Stage "A1": "Extending the Applicability Condition"
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
component section plane files
rt-conversion context-sensitive parallel r-conversion for terms cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? ) cpc_cpc
rt-computation uncounted context-sensitive parallel rt-computation refinement for lenvs lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? ) lsubsx_lfsx lsubsx_lsubsx


strongly normalizing for lenvs on referred entries lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ ) lfsx_drops lfsx_fqup lfsx_lfpxs lfsx_lfsx


strongly normalizing for term vectors csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) csx_cnx_vector csx_csx_vector


strongly normalizing for terms csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ ) csx_simple csx_simple_theq csx_drops csx_lsubr csx_lfdeq csx_aaa csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_lfpxs csx_csx


for lenvs on referred entries lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? ) lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lpxs lfpxs_lfpxs


for lenvs on all entries lpxs ( ⦃?,?⦄ ⊢ ⬈*[?] ? )


for terms cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? ) cpxs_tdeq cpxs_theq cpxs_theq_vector cpxs_drops cpxs_fqus cpxs_lsubr cpxs_lfdeq cpxs_aaa cpxs_lpx cpxs_lfpx cpxs_cnx cpxs_cpxs
rt-transition uncounted parallel rst-transition for closures fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ ) fpbq_aaa


proper for closures fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ ) fpb_lfdeq

context-sensitive parallel r-transition for lenvs on referred entries lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_aaa lfpr_lfpx lfpr_lfpr


for binders cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )


for terms cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? ) cpr_drops

t-bound context-sensitive parallel rt-transition for terms cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) cpm_simple cpm_drops cpm_lsubr cpm_lfxs cpm_cpx

uncounted context-sensitive parallel rt-transition normal form for terms cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ ) cnx_simple cnx_drops cnx_cnx


for lenvs on referred entries lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? ) lfpx_length lfpx_drops lfpx_fqup lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx


for lenvs on all entries lpx ( ⦃?,?⦄ ⊢ ⬈[?] ? )


for binders cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )


for terms cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? ) cpx_simple cpx_drops cpx_fqus cpx_lsubr cpx_lfxs cpx_lfeq

counted context-sensitive parallel rt-transition for terms cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) cpg_simple cpg_drops cpg_lsubr
iterated static typing iterated generic extension of a context-sensitive relation for lenvs on referred entries tc_lfxs ( ? ⦻**[?,?] ? ) tc_lfxs_length tc_lfxs_lex tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs
static typing generic reducibility restricted refinement for lenvs lsubc ( ? ⊢ ? ⫃[?] ? ) lsubc_drops lsubc_lsubr lsubc_lsuba


candidates gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) gcp_aaa


computation properties gcp

atomic arity assignment restricted refinement for lenvs lsuba ( ? ⊢ ? ⫃⁝ ? ) lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba


for terms aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) aaa_drops aaa_fqus aaa_lfdeq aaa_aaa

degree-based equivalence for closures on referred entries ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ ) ffdeq_fqup ffdeq_ffdeq


for lenvs on referred entries lfdeq ( ? ≛[?,?,?] ? ) lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq

syntactic equivalence for lenvs on referred entries lfeq ( ? ≡[?] ? ) lfeq_fqup lfeq_lfeq

generic extension of a context-sensitive relation for lenvs on referred entries lfxs ( ? ⦻*[?,?] ? ) lfxs_length lfxs_lex lfxs_drops lfxs_fqup flxs_fle lfxs_lfxs

context-sensitive free variables inclusion for restricted closures fle ( ⦃?,?⦄ ⊆ ⦃?,?⦄ ) fle_drops fle_fqup fle_fle


restricted refinement for lenvs lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) lsubf_lsubr lsubf_frees lsubf_lsubf


for terms frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) frees_drops frees_fqup frees_frees

local environments restricted refinement lsubr ( ? ⫃ ? ) lsubr_length lsubr_drops lsubr_lsubr
s-computation iterated structural successor for closures fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) fqus_weight fqus_drops fqus_fqup fqus_fqus


proper for closures fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) fqup_weight fqup_drops fqup_fqup
s-transition structural successor for closures fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) fquq_length fquq_weight


proper for closures fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) fqu_length fqu_weight
relocation generic slicing for lenvs drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) drops_lstar drops_weight drops_length drops_cext2 drops_lexs drops_lreq drops_drops drops_vector

generic relocation for binders lifts_bind ( ⬆*[?] ? ≡ ? ) lifts_weight_bind lifts_lifts_bind


for term vectors lifts_vector ( ⬆*[?] ? ≡ ? ) lifts_lifts_vector


for terms lifts ( ⬆*[?] ? ≡ ? ) lifts_simple lifts_weight lifts_tdeq lifts_lifts

syntactic equivalence for lenvs on selected entries lreq ( ? ≡[?] ? ) lreq_length lreq_lreq

generic entrywise extension for lenvs of one contex-sensitive relation lex ( ? ⦻[?] ? ) lex_tc


for lenvs of two contex-sensitive relations lexs ( ? ⦻*[?,?,?] ? ) lexs_tc lexs_length lexs_lexs
syntax equivalence up to exclusion binders for lenvs lveq ( ? ≋ⓧ*[?,?] ? ) lveq_length lveq_lveq

append for lenvs append ( ? @@ ? ) append_length

head equivalence for terms theq ( ? ⩳[?,?] ? ) theq_simple theq_tdeq theq_theq theq_simple_vector

degree-based equivalence tdeq_ext ( ? ≛[?,?] ? ) ( ? ⊢ ? ≛[?,?] ? )


tdeq ( ? ≛[?,?] ? ) tdeq_tdeq

closures cl_weight ( ♯{?,?,?} )


cl_restricted_weight ( ♯{?,?} )

global environments genv

local environments ceq_ext ceq_ext_ceq_ext


cext2


lenv_length ( |?| )


lenv_weight ( ♯{?} )


lenv

binders for local environments ext2 ext2_tc ext2_ext2


bind bind_weight

terms term_vector ( Ⓐ?.? )


term_simple ( 𝐒⦃?⦄ )


term_weight ( ♯{?} )


term

items item_sd


item_sh


item

atomic arities aarity
[Spacer]

[Valid XHTML 1.1] [Valid CSS level 2] [Generated from XML via XSL] [PNG used here] [Viewable with any browser]

Last update: Wed, 17 Jan 2018 20:27:14 +0100