| component | section | plane | files |
|
| iterated dynamic typing | context-sensitive iterated native type assignment | for terms | ntas ( ❪?,?❫ ⊢ ? :*[?,?,?] ? ) | ntas_cpcs ntas_nta ntas_nta_ind ntas_ntas ntas_preserve |
| dynamic typing | context-sensitive native type assignment | for terms | nta ( ❪?,?❫ ⊢ ? :[?,?] ? ) | nta_drops nta_aaa nta_fsb nta_cpms nta_cpcs nta_preserve nta_preserve_cpcs nta_ind nta_eval |
| context-sensitive native validity | restricted refinement for lenvs | lsubv ( ? ⊢ ? ⫃![?,?] ? ) | lsubv_drops lsubv_lsubr lsubv_lsuba lsubv_cpms lsubv_cpcs lsubv_cnv lsubv_lsubv |
|
| for terms | cnv ( ❪?,?❫ ⊢ ? ![?,?] ) | cnv_acle cnv_drops cnv_fqus cnv_aaa cnv_fsb cnv_cpm_trans cnv_cpm_conf cnv_cpm_teqx cnv_cpm_teqx_trans cnv_cpm_teqx_conf cnv_cpms_teqx cnv_cpms_conf cnv_cpms_teqx_conf cnv_cpmre cnv_cpmuwe cnv_cpmuwe_cpmre cnv_cpts cnv_cpes cnv_cpcs cnv_preserve_sub cnv_preserve cnv_preserve_cpes cnv_preserve_cpcs cnv_eval |
| rt-equivalence | context-sensitive parallel r-equivalence | for terms | cpcs ( ❪?,?❫ ⊢ ? ⬌*[?] ? ) | cpcs_drops cpcs_lsubr cpcs_aaa cpcs_csx cpcs_cprs cpcs_lprs cpcs_cpc cpcs_cpcs |
| t-bound context-sensitive parallel rt-equivalence | for terms | cpes ( ❪?,?❫ ⊢ ? ⬌*[?,?,?] ? ) | cpes_aaa cpes_cpms cpes_cpes |
| rt-conversion | context-sensitive parallel r-conversion | for terms | cpc ( ❪?,?❫ ⊢ ? ⬌[?] ? ) | cpc_cpc |
| rt-computation | context-sensitive parallel t-computation | for terms | cpts ( ❪?,?❫ ⊢ ? ⬆*[?,?] ? ) | cpts_drops cpts_aaa cpts_cpms |
| context-sensitive parallel r-computation | evaluation for terms | cprre | cprre_csx cprre_cpms cprre_cprre |
|
| for lenvs on all entries | lprs ( ❪?,?❫ ⊢ ➡*[?,?] ? ) | lprs_tc lprs_ctc lprs_length lprs_drops lprs_aaa lprs_lpr lprs_lpxs lprs_cpms lprs_cprs lprs_lprs |
|
| for binders | cprs_ext ( ❪?,?❫ ⊢ ? ➡*[?,?] ?) |
|
|
| for terms | cprs | cprs_ctc cprs_teqw cprs_drops cprs_cpr cprs_lpr cprs_cnr cprs_cprs |
| t-bound context-sensitive parallel rt-computation | t-unbound whd evaluation for terms | cpmuwe ( ❪?,?❫ ⊢ ? ➡*𝐍𝐖*[?,?] ? ) | cpmuwe_csx cpmuwe_cpmuwe |
|
| t-unbound whd normal form for terms | cnuw ( ❪?,?❫ ⊢ ➡𝐍𝐖*[?] ? ) | cnuw_drops cnuw_simple cnuw_cnuw |
|
| t-bpund evaluation for terms | cpmre ( ❪?,?❫ ⊢ ? ➡*𝐍[?,?] ? ) | cpmre_aaa |
|
| for terms | cpms ( ❪?,?❫ ⊢ ? ➡*[?,?] ? ) | cpms_drops cpms_lsubr cpms_reqg cpms_aaa cpms_lpr cpms_cpxs cpms_fpbs cpms_fpbg cpms_cpms |
| extended context-sensitive parallel rst-computation | strongly normalizing for closures | fsb ( ≥𝐒 ❪?,?,?❫ ) | fsb_feqg fsb_aaa fsb_csx fsb_fpbg |
|
| proper for closures | fpbg ( ❪?,?,?❫ > ❪?,?,?❫ ) | fpbg_fqup fpbg_fqus fpbg_feqg fpbg_cpm fpbg_cpxs fpbg_lpxs fpbg_fpbs fpbg_fpbg |
|
| for closures | fpbs ( ❪?,?,?❫ ≥ ❪?,?,?❫ ) | fpbs_fqup fpbs_fqus fpbs_feqg fpbs_aaa fpbs_cpx fpbs_fpbc fpbs_cpxs fpbs_lpxs fpbs_csx fpbs_fpbs |
| extended context-sensitive parallel rt-computation | compatibility for lenvs | jsx ( ? ⊢ ? ⊒ ? ) | jsx_drops jsx_lsubr jsx_csx jsx_rsx jsx_jsx |
|
| strongly normalizing for lenvs on referred entries | rsx ( ? ⊢ ⬈*𝐒[?] ? ) | rsx_length rsx_drops rsx_fqup rsx_cpxs rsx_csx rsx_rsx |
|
| strongly normalizing for term vectors | csx_vector ( ❪?,?❫ ⊢ ⬈*𝐒 ? ) | csx_cnx_vector csx_csx_vector |
|
| strongly normalizing for terms | csx ( ❪?,?❫ ⊢ ⬈*𝐒 ? ) | csx_simple csx_simple_teqo csx_drops csx_fqus csx_lsubr csx_reqg csx_feqg csx_aaa csx_gcp csx_gcr csx_lpx csx_cnx csx_fpb csx_cpxs csx_lpxs csx_csx |
|
| for lenvs on all entries | lpxs ( ❪?,?❫ ⊢ ⬈* ? ) | lpxs_length lpxs_drops lpxs_reqg lpxs_feqg lpxs_aaa lpxs_lpx lpxs_cpxs lpxs_lpxs |
|
| for binders | cpxs_ext ( ❪?,?❫ ⊢ ? ⬈* ? ) |
|
|
| for terms | cpxs ( ❪?,?❫ ⊢ ? ⬈* ? ) | cpxs_teqg cpxs_teqo cpxs_teqo_vector cpxs_drops cpxs_fqus cpxs_lsubr cpxs_reqg cpxs_feqg cpxs_aaa cpxs_lpx cpxs_cnx cpxs_cpxs |
| rt-transition | context-sensitive parallel t-transition | for terms | cpt ( ❪?,?❫ ⊢ ? ⬆[?,?] ? ) | cpt_drops cpt_fqu cpt_cpm |
| context-sensitive parallel r-transition | normal form for terms | cnr ( ❪?,?❫ ⊢ ➡𝐍[?,?] ? ) | cnr_simple cnr_teqg cnr_teqx cnr_drops |
|
| for lenvs on all entries | lpr ( ❪?,?❫ ⊢ ➡[?,?] ? ) | lpr_length lpr_drops lpr_fquq lpr_aaa lpr_lpx lpr_fpb lpr_fpbc lpr_lpr |
|
| for binders | cpr_ext |
|
|
| for terms | cpr | cpr_drops cpr_drops_basic cpr_teqg cpr_cpr |
| t-bound context-sensitive parallel rt-transition | for terms | cpm ( ❪?,?❫ ⊢ ? ➡[?,?] ? ) | cpm_simple cpm_teqx cpm_drops cpm_lsubr cpm_fsle cpm_aaa cpm_cpx cpm_fpb cpm_fpbc |
| extended parallel rst-transition | proper for closures | fpbc ( ❪?,?,?❫ ≻ ❪?,?,?❫ ) | fpbc_fqup fpbc_feqg fpbc_lpx fpbc_fpb |
|
| for closures | fpb ( ❪?,?,?❫ ≽ ❪?,?,?❫ ) | fpb_fqup fpb_feqg fpb_aaa fpb_lpx |
| extended context-sensitive parallel rt-transition | normal form for terms | cnx ( ❪?,?❫ ⊢ ⬈𝐍 ? ) | cnx_simple cnx_drops cnx_basic cnx_cnx |
|
| for lenvs on referred entries | rpx ( ❪?,?❫ ⊢ ⬈[?] ? ) | rpx_length rpx_drops rpx_fqup rpx_fsle rpx_reqg rpx_reqx rpx_lpx rpx_rpx |
|
| for lenvs on all entries | lpx ( ❪?,?❫ ⊢ ⬈ ? ) | lpx_length lpx_drops lpx_fquq lpx_fsle lpx_reqg lpx_aaa |
|
| for binders | cpx_ext ( ❪?,?❫ ⊢ ? ⬈ ? ) |
|
|
| for terms | cpx ( ❪?,?❫ ⊢ ? ⬈ ? ) | cpx_simple cpx_drops cpx_drops_basic cpx_fqus cpx_lsubr cpx_req cpx_reqg cpx_feqg |
| bound context-sensitive parallel rt-transition | for terms | cpg ( ❪?,?❫ ⊢ ? ⬈[?,?,?] ? ) | cpg_simple cpg_drops cpg_lsubr |
![[\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")