[ "crf ( ? β’ πβ¦?β¦ )" "crf_append" "cif ( ? β’ πβ¦?β¦ )" "cif_append" * ]
}
]
+ [ { "focalized reduction" * } {
+ [ "lfpr_alt ( β¦?β¦ β‘β‘ β¦?β¦ )" * ]
+ [ "fpr ( β¦?,?β¦ β‘ β¦?,?β¦ )" * ]
+ }
+ ]
[ { "context-free normal forms" * } {
[ "thnf ( ππβ¦?β¦ )" * ]
}
}
]
[ { "stratified static type assignment" * } {
- [ "ssta ( β¦?,?β¦ β’ ? β’[?,?] ? )" "ssta_lift" "ssta_ltpss" "ssta_aaa" "ssta_ssta" * ]
+ [ "ssta ( β¦?,?β¦ β’ ? β’[?,?] ? )" "ssta_lift" "ssta_ltpss_dx" "ssta_ltpss_sn" "ssta_aaa" "ssta_ssta" * ]
}
]
[ { "local env. ref. for atomic arity assignment" * } {
}
]
[ { "atomic arity assignment" * } {
- [ "aaa ( ? β’ ? β ? )" "aaa_lift" "aaa_lifts" "aaa_ltpss" "aaa_aaa" * ]
+ [ "aaa ( ? β’ ? β ? )" "aaa_lift" "aaa_lifts" "aaa_ltpss_dx" "aaa_ltpss_sn" "aaa_aaa" * ]
}
]
[ { "parameters" * } {
}
]
[ { "partial unfold" * } {
- [ "ltpss ( ? βΆ*[?,?] ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_tpss" "ltpss_ltpss" * ]
+ [ "ltpss_sn ( ? β’ βΆ*[?,?] ? )" "ltpss_sn_ldrop" "ltpss_sn_tps" "ltpss_sn_tpss" "ltpss_sn_ltpss_sn" "ltpss_sn_alt ( ? β’ βΆβΆ*[?,?] ? )" * ]
+ [ "ltpss_dx ( ? βΆ*[?,?] ? )" "ltpss_dx_ldrop" "ltpss_dx_tps" "ltpss_dx_tpss" "ltpss_dx_ltpss_dx" * ]
[ "tpss ( ? β’ ? βΆ*[?,?] ? )" "tpss_alt ( ? β’ ? βΆβΆ*[?,?] ? )" "tpss_lift" "tpss_tpss" * ]
}
]
}
]
[ { "local env. ref. for substitution" * } {
- [ "lsubs ( ? βΌ[?,?] ? )" "lsubs_lsubs" "lsubs_sfr ( β½[?,?] ? )" * ]
+ [ "lsubs ( ? βΌ[?,?] ? )" "(lsubs_lsubs)" "lsubs_sfr ( β½[?,?] ? )" * ]
}
]
[ { "basic term relocation" * } {
class "red"
[ { "grammar" * } {
[ { "same head term form" * } {
- [ "tshf ( ? β ? )" "tshf_tshf" * ]
+ [ "tshf ( ? β ? )" "(tshf_tshf)" * ]
}
]
[ { "same top term constructor" * } {
]
[ { "internal syntax" * } {
[ "genv" * ]
- [ "lenv" "lenv_weight ( #{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" * ]
+ [ "lenv" "lenv_weight ( #{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" "lenv_px_bi" * ]
[ "term" "term_weight ( #{?} )" "term_simple ( πβ¦?β¦ )" "term_vector" * ]
[ "item" * ]
}