[\lambda\delta home]
cic:/BOLOGNA/lambdadelta/basic_1/ (core λδ version 1)

home news specification

documentation implementation
foreword milestones version 2 (background - syntax - core - applications)
version 2 helena Open Symbolic Notation (OSN)
citations visibility version 1 (background - core) (static HELM directory) version 1 library (static LDDL directory)
Abstract Syntax and Behavior [butterfly]
This is a summary of available syntactic items and reductions (block structure).
domain block leader →ζ * annotator (with →ϵ *) applicator (with →θ *) reference * reduction
{X | Γ ⊢ ⊤} exclusion Γ ⊢ χ yes no no no no
{X | Γ ⊢ X : W} typed abstraction Γ ⊢ λW no <W> (V) #i →β *
{X | Γ ⊢ X = V} abbreviation Γ ⊢ δV yes no no #i →δ
no sort Γ ⊢ ⋆k no no no no no
* In terms only.
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline.
category objects

sizes files 120 characters 198089 nodes 1449099
propositions theorems 81 lemmas 618 total 699
concepts declared 39 defined 47 total 86
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
component plane files
examples terms with special features levels_ex0 ty3_ex1 nf2_ex2

dynamic typing well-formed contexts wf3_defs wf3_props

context ref. for native type assignment csubt_defs csubt_props csubt_arity_props

native type assignment ty3_defs ty3_props ty3_gen ty3_gen_context ty3_gen_nf2 ty3_lift ty3_subst0 ty3_arity_props ty3_nf2_gen ty3_sred ty3_sred_props ty3_dec
equivalence context-sensitive equivalence pc3_defs pc3_props pc3_gen pc3_gen_context pc3_subst0

context-free equivalence pc1_defs pc1_props

computation context ref. for reducibility csubc_defs csubc_props

reducibility sc3_defs sc3_props sc3_arity

strongly normalizing computation sn3_defs sn3_gen sn3_props

context-sensitive computation pr3_defs pr3_props pr3_gen pr3_gen_context pr3_iso pr3_subst1 pr3_confluence

context-free computation pr1_defs pr1_props pr1_confluence
reduction normal forms for context-sensitive reduction nf2_defs nf2_props nf2_gen nf2_dec

context-sensitive reduction pr2_defs pr2_gen pr2_gen_context pr2_lift pr2_subst1 pr2_confluence

normal forms for context-free reduction nf0_dec

context-free reduction wcpr0_defs

pr0_defs pr0_gen pr0_lift pr0_subst0 pr0_subst1 pr0_confluence
unfold iterated static type assignment sty1_defs sty1_props
static typing static type assignment sty0_defs sty0_props

context ref. for binary arity assignment csuba_defs csuba_props

binary arity assignment arity_defs arity_props arity_gen arity_subst0 arity_sred

binary arity levels_defs llt_defs aprem_defs

parameters parameter_defs

basic context ref. csubv_defs
multiple substitution iterated context slicing drop1_defs drop1_props

generic term relocation lift1_defs lift1_props
substitution ordinary substitution subst_defs subst_props

csubst1_defs csubst1_props

subst1_defs subst1_gen subst1_lift subst1_subst1 subst1_confluence

normal forms for ordinary strict substitution dnf_dec

ordinary strict substitution fsubst0_defs


subst0_defs subst0_gen subst0_tlt subst0_lift subst0_subst0 subst0_confluence

basic local env. slicing getl_defs getl_props

drop_defs drop_props

basic term relocation lift_defs lift_props lift_gen lift_tlt
grammar closures flt_defs

contexts contexts_defs clt_defs ctail_defs app_defs cnt_defs

terms tlist_defs

terms_defs tlt_defs iso_defs

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

Last update: Sat, 15 Jun 2019 15:22:10 +0200