| component | section | plane | files |
|
| iterated static typing | iterated generic extension of a context-sensitive relation | for lenvs on referred entries | rexs ( ? ⪤*[?,?] ? ) | rexs_length rexs_lex rexs_drops rexs_fqup rexs_rexs |
| 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_reqg aaa_feqg aaa_aaa aaa_dec |
| sort-irrelevant equivalence | for closures on referred entries | feqx ( ❪?,?,?❫ ≅ ❪?,?,?❫ ) | feqx_feqx |
|
| for lenvs on referred entries | reqx ( ? ≅[?] ? ) | reqx_reqx |
| syntactic equivalence | for lenvs on referred entries | req ( ? ≡[?] ? ) |
|
| generic equivalence | for closures on referred entries | feqg ( ❪?,?,?❫ ≛[?] ❪?,?,?❫ ) | feqg_length feqg_fqu feqg_fqup feqg_fqus feqg_feqg |
|
| for lenvs on referred entries | reqg ( ? ≛[?,?] ? ) | reqg_length reqg_drops reqg_fqup reqg_fqus reqg_reqg |
| generic extension of a context-sensitive relation | for lenvs on referred entries | rex ( ? ⪤[?,?] ? ) | rex_length rex_lex rex_drops rex_fqup rex_fsle rex_rex |
| context-sensitive free variables | inclusion for restricted closures | fsle ( ❪?,?❫ ⊆ ❪?,?❫ ) | fsle_length fsle_drops fsle_fqup fsle_fsle |
|
| restricted refinement for lenvs | lsubf ( ❪?,?❫ ⫃𝐅+ ❪?,?❫ ) | lsubf_lsubr lsubf_frees lsubf_lsubf |
|
| for terms | frees ( ? ⊢ 𝐅+❪?❫ ≘ ? ) | frees_append 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 fqu_teqg |
| relocation | generic and uniform slicing | for lenvs | drops ( ⇩*[?,?] ? ≘ ? ) ( ⇩[?] ? ≘ ? ) | drops_ctc drops_ltc drops_weight drops_length drops_cext2 drops_sex drops_lex drops_seq drops_drops drops_vector |
| basic relocation | for terms | lifts_basic ( ⇧[?,?] ? ≘ ? ) |
|
| generic and uniform 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_teqg lifts_teqx lifts_teqw lifts_teqo lifts_lifts |
| syntactic equivalence | for lenvs on selected entries | seq ( ? ≡[?] ? ) | seq_length seq_seq |
| generic entrywise extension | for lenvs of one contex-sensitive relation | lex ( ? ⪤[?] ? ) | lex_tc lex_length lex_lex |
|
| for lenvs of two contex-sensitive relations | sex ( ? ⪤[?,?,?] ? ) | sex_tc sex_length sex_sex |
| syntax | applicability condition | preorder | acle ( ? ⊆ ? ) | acle_acle |
|
| properties | ac ( 𝟏 ) ( 𝟐 ) ( 𝛚 ) |
|
| equivalence up to exclusion binders | for lenvs | lveq ( ? ≋ⓧ*[?,?] ? ) | lveq_length lveq_lveq |
| append | for restricted closures | fold ( ? + ? ) | fold_append |
|
| for lenvs | append ( ? + ? ) | append_length |
| sort-irrelevant outer equivalence | for terms | teqo ( ? ~ ? ) | teqo_simple teqo_teqg teqo_teqo teqo_simple_vector |
| sort-irrelevant whd equivalence | for terms | teqw ( ? ≃ ? ) | teqw_simple teqw_teqg teqw_teqw |
| sort-irrelevant equivalence | | teqx_ext ( ? ≅ ? ) ( ? ⊢ ? ≅ ? ) |
|
|
| | teqx ( ? ≅ ? ) | teqx_teqx |
| syntactic equivalence | | teq_ext ( ? ≡ ? ) ( ? ⊢ ? ≡ ? ) | teq_ext_teq_ext |
|
| | teq ( ? ≡ ? ) | teq_teq |
| generic equivalence | | teqg_ext ( ? ≛[?] ? ) ( ? ⊢ ? ≛[?] ? ) |
|
|
| | teqg ( ? ≛[?] ? ) | teqg_teqg |
| closures | | cl_weight ( ♯❨?,?,?❩ ) |
|
|
| | cl_restricted_weight ( ♯❨?,?❩ ) |
|
| global environments | | genv_length ( |?| ) |
|
|
| | genv_weight ( ♯❨?❩ ) |
|
|
| | genv |
|
| local environments | | 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 |
|
| sorts | degree | sd | sd_d sd_lt |
|
| hierarchy | sh ( ⫯[?]? ) | sh_props sh_lt |
| atomic arities | | aarity |
|
![[\lambda\delta home]](http://helm.cs.unibo.it/lambdadelta/images/crux_32.png "\lambda\delta home")
![[Spacer]](http://helm.cs.unibo.it/lambdadelta/images/rainbow.png "\lambda\delta rainbow rule")
![[butterfly]](http://helm.cs.unibo.it/lambdadelta/images/b4.png "\lambda\delta butterfly")
![[Generated from XML via XSL]](http://helm.cs.unibo.it/lambdadelta/images/xml_xsl2.png "Generated from XML via XSL")
![[PNG used here]](http://helm.cs.unibo.it/lambdadelta/images/PNGnow2.png "PNG used here")
![[Viewable with any browser]](http://www.anybrowser.org/campaign/bvgraphics/abtfile.png "Viewable with any browser")