- <td class="ssnn top water">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic water">
- <br />
- </td>
- <td class="snns top italic water">irreducible forms for context-sensitive reduction</td>
- <td class="snns top water">cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )</td>
- <td class="snnn top water">cir_lift</td>
- <td class="snnn top water">
- <br />
- </td>
- <td class="ssnn top water">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic water">
- <br />
- </td>
- <td class="snns top italic water">reducible forms for context-sensitive reduction</td>
- <td class="snns top water">crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )</td>
- <td class="snnn top water">crr_lift</td>
- <td class="snnn top water">
- <br />
- </td>
- <td class="ssnn top water">
- <br />
- </td>
- </tr>
- <tr>
- <td class="snns top capitalize italic green">unfold</td>
- <td class="snns top italic green">unfold</td>
- <td class="snns top green">unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )</td>
- <td class="snnn top green">
- <br />
- </td>
- <td class="snnn top green">
- <br />
- </td>
- <td class="ssnn top green">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic green">
- <br />
- </td>
- <td class="snns top italic green">iterated static type assignment</td>
- <td class="snns top green">lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )</td>
- <td class="snnn top green">lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas</td>
- <td class="snnn top green">
- <br />
- </td>
- <td class="ssnn top green">
- <br />
- </td>
- </tr>
- <tr>
- <td class="snns top capitalize italic grass">static typing</td>
- <td class="snns top italic grass">local env. ref. for degree assignment</td>
- <td class="snns top grass">lsubd ( ? ⊢ ? ⫃▪[?,?] ? )</td>
- <td class="snnn top grass">lsubd_da lsubd_lsubd</td>
- <td class="snnn top grass">
- <br />
- </td>
- <td class="ssnn top grass">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic grass">
- <br />
- </td>
- <td class="snns top italic grass">degree assignment</td>
- <td class="snns top grass">da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )</td>
- <td class="snnn top grass">da_lift da_aaa da_da</td>
- <td class="snnn top grass">
- <br />
- </td>
- <td class="ssnn top grass">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic grass">
- <br />
- </td>
- <td class="snns top italic grass">parameters</td>
- <td class="snns top grass">sh</td>
- <td class="snnn top grass">sd</td>
- <td class="snnn top grass">
- <br />
- </td>
- <td class="ssnn top grass">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic grass">
- <br />
- </td>
- <td class="snns top italic grass">local env. ref. for atomic arity assignment</td>
- <td class="snns top grass">lsuba ( ? ⊢ ? ⫃⁝ ? )</td>
- <td class="snnn top grass">lsuba_aaa lsuba_lsuba</td>
- <td class="snnn top grass">
- <br />
- </td>
- <td class="ssnn top grass">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic grass">
- <br />
- </td>
- <td class="snns top italic grass">atomic arity assignment</td>
- <td class="snns top grass">aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )</td>
- <td class="snnn top grass">aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa</td>
- <td class="snnn top grass">
- <br />
- </td>
- <td class="ssnn top grass">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic grass">
- <br />
- </td>
- <td class="snns top italic grass">restricted local env. ref.</td>
- <td class="snns top grass">lsubr ( ? ⫃ ? )</td>
- <td class="snnn top grass">lsubr_lsubr</td>
- <td class="snnn top grass">
- <br />
- </td>
- <td class="ssnn top grass">
- <br />
- </td>
- </tr>
- <tr>
- <td class="snns top capitalize italic yellow">multiple substitution</td>
- <td class="snns top italic yellow">lazy equivalence</td>
- <td class="snns top yellow">fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )</td>
- <td class="snnn top yellow">fleq_fleq</td>
- <td class="snnn top yellow">
- <br />
- </td>
- <td class="ssnn top yellow">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic yellow">
- <br />
- </td>
- <td class="nnns top italic yellow">
- <br />
- </td>
- <td class="snns top yellow">lleq ( ? ≡[?,?] ? )</td>
- <td class="snnn top yellow">lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq</td>
- <td class="snnn top yellow">
- <br />
- </td>
- <td class="ssnn top yellow">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic yellow">
- <br />
- </td>
- <td class="snns top italic yellow">lazy pointwise extension of a relation</td>
- <td class="snns top yellow">llpx_sn</td>
- <td class="snnn top yellow">llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_lreq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor</td>
- <td class="snnn top yellow">
- <br />
- </td>
- <td class="ssnn top yellow">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic yellow">
- <br />
- </td>
- <td class="snns top italic yellow">pointwise union for local environments</td>
- <td class="snns top yellow">llor ( ? ⋓[?,?] ? ≡ ? )</td>
- <td class="snnn top yellow">llor_alt llor_drop</td>
- <td class="snnn top yellow">
- <br />
- </td>
- <td class="ssnn top yellow">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic yellow">
- <br />
- </td>
- <td class="snns top italic yellow">context-sensitive exclusion from free variables</td>
- <td class="snns top yellow">frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )</td>
- <td class="snnn top yellow">frees_append frees_lreq frees_lift</td>
- <td class="snnn top yellow">
- <br />
- </td>
- <td class="ssnn top yellow">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic yellow">
- <br />
- </td>
- <td class="snns top italic yellow">contxt-sensitive multiple rt-substitution</td>
- <td class="snns top yellow">cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )</td>
- <td class="snnn top yellow">cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )</td>
- <td class="snnn top yellow">cpys_lift cpys_cpys</td>
- <td class="ssnn top yellow">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic yellow">
- <br />
- </td>
- <td class="snns top italic yellow">iterated structural successor for closures</td>
- <td class="snns top yellow">fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )</td>
- <td class="snnn top yellow">fqus_alt fqus_fqus</td>
- <td class="snnn top yellow">
- <br />
- </td>
- <td class="ssnn top yellow">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic yellow">
- <br />
- </td>
- <td class="nnns top italic yellow">
- <br />
- </td>
- <td class="snns top yellow">fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )</td>
- <td class="snnn top yellow">fqup_fqup</td>
- <td class="snnn top yellow">
- <br />
- </td>
- <td class="ssnn top yellow">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic yellow">
- <br />
- </td>
- <td class="snns top italic yellow">iterated local env. slicing</td>
- <td class="snns top yellow">drops ( ⬇*[?,?] ? ≡ ? )</td>
- <td class="snnn top yellow">drops_drop drops_drops</td>
- <td class="snnn top yellow">
- <br />
- </td>
- <td class="ssnn top yellow">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic yellow">
- <br />
- </td>
- <td class="snns top italic yellow">generic term relocation</td>
- <td class="snns top yellow">lifts_vector ( ⬆*[?] ? ≡ ? )</td>
- <td class="snnn top yellow">lifts_lift_vector</td>
- <td class="snnn top yellow">
- <br />
- </td>
- <td class="ssnn top yellow">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic yellow">
- <br />
- </td>
- <td class="nnns top italic yellow">
- <br />
- </td>
- <td class="snns top yellow">lifts ( ⬆*[?] ? ≡ ? )</td>
- <td class="snnn top yellow">lifts_lift lifts_lifts</td>
- <td class="snnn top yellow">
- <br />
- </td>
- <td class="ssnn top yellow">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic yellow">
- <br />
- </td>
- <td class="snns top italic yellow">support for multiple relocation</td>
- <td class="snns top yellow">mr2 ( @⦃?,?⦄ ≡ ? )</td>
- <td class="snnn top yellow">mr2_plus ( ? + ? )</td>
- <td class="snnn top yellow">mr2_minus ( ? ▭ ? ≡ ? )</td>
- <td class="ssnn top yellow">mr2_mr2</td>
- </tr>
- <tr>
- <td class="snns top capitalize italic orange">substitution</td>
- <td class="snns top italic orange">structural successor for closures</td>
- <td class="snns top orange">fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )</td>
- <td class="snnn top orange">fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )</td>
- <td class="snnn top orange">
- <br />
- </td>
- <td class="ssnn top orange">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic orange">
- <br />
- </td>
- <td class="nnns top italic orange">
- <br />
- </td>
- <td class="snns top orange">fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )</td>
- <td class="snnn top orange">
- <br />
- </td>
- <td class="snnn top orange">
- <br />
- </td>
- <td class="ssnn top orange">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic orange">
- <br />
- </td>
- <td class="snns top italic orange">global env. slicing</td>
- <td class="snns top orange">gget ( ⬇[?] ? ≡ ? )</td>
- <td class="snnn top orange">gget_gget</td>
- <td class="snnn top orange">
- <br />
- </td>
- <td class="ssnn top orange">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic orange">
- <br />
- </td>
- <td class="snns top italic orange">contxt-sensitive ordinary rt-substitution</td>
- <td class="snns top orange">cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )</td>
- <td class="snnn top orange">cpy_lift cpy_nlift cpy_cpy</td>
- <td class="snnn top orange">
- <br />
- </td>
- <td class="ssnn top orange">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic orange">
- <br />
- </td>
- <td class="snns top italic orange">local env. ref. for rt-substitution</td>
- <td class="snns top orange">lsuby ( ? ⊆[?,?] ? )</td>
- <td class="snnn top orange">lsuby_lsuby</td>
- <td class="snnn top orange">
- <br />
- </td>
- <td class="ssnn top orange">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic orange">
- <br />
- </td>
- <td class="snns top italic orange">pointwise extension of a relation</td>
- <td class="snns top orange">lpx_sn</td>
- <td class="snnn top orange">lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn</td>
- <td class="snnn top orange">
- <br />
- </td>
- <td class="ssnn top orange">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic orange">
- <br />
- </td>
- <td class="snns top italic orange">basic local env. slicing</td>
- <td class="snns top orange">drop ( ⬇[?,?,?] ? ≡ ? )</td>
- <td class="snnn top orange">drop_append drop_lreq drop_drop</td>
- <td class="snnn top orange">
- <br />
- </td>
- <td class="ssnn top orange">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic orange">
- <br />
- </td>
- <td class="snns top italic orange">basic term relocation</td>
- <td class="snns top orange">lift_vector ( ⬆[?,?] ? ≡ ? )</td>
- <td class="snnn top orange">lift_lift_vector</td>
- <td class="snnn top orange">
- <br />
- </td>
- <td class="ssnn top orange">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic orange">
- <br />
- </td>
- <td class="nnns top italic orange">
- <br />
- </td>
- <td class="snns top orange">lift ( ⬆[?,?] ? ≡ ? )</td>
- <td class="snnn top orange">lift_neq lift_lift</td>
- <td class="snnn top orange">
- <br />
- </td>
- <td class="ssnn top orange">
- <br />
- </td>
- </tr>
- <tr>
- <td class="snns top capitalize italic red">grammar</td>
- <td class="snns top italic red">equivalence for local environments</td>
- <td class="snns top red">lreq ( ? ⩬[?,?] ? )</td>
- <td class="snnn top red">lreq_lreq</td>
- <td class="snnn top red">
- <br />
- </td>
- <td class="ssnn top red">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic red">
- <br />
- </td>
- <td class="snns top italic red">same top term structure</td>
- <td class="snns top red">tsts ( ? ≂ ? )</td>
- <td class="snnn top red">tsts_tsts tsts_vector</td>
- <td class="snnn top red">
- <br />
- </td>
- <td class="ssnn top red">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic red">
- <br />
- </td>
- <td class="snns top italic red">closures</td>
- <td class="snns top red">cl_weight ( ♯{?,?,?} )</td>
- <td class="snnn top red">cl_restricted_weight ( ♯{?,?} )</td>
- <td class="snnn top red">
- <br />
- </td>
- <td class="ssnn top red">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic red">
- <br />
- </td>
- <td class="snns top italic red">internal syntax</td>
- <td class="snns top red">genv</td>
- <td class="snnn top red">
- <br />
- </td>
- <td class="snnn top red">
- <br />
- </td>
- <td class="ssnn top red">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic red">
- <br />
- </td>
- <td class="nnns top italic red">
- <br />
- </td>
- <td class="snns top red">lenv</td>
- <td class="snnn top red">lenv_weight ( ♯{?} )</td>
- <td class="snnn top red">lenv_length ( |?| )</td>
- <td class="ssnn top red">lenv_append ( ? @@ ? )</td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic red">
- <br />
- </td>
- <td class="nnns top italic red">
- <br />
- </td>
- <td class="snns top red">term</td>
- <td class="snnn top red">term_weight ( ♯{?} )</td>
- <td class="snnn top red">term_simple ( 𝐒⦃?⦄ )</td>
- <td class="ssnn top red">term_vector ( Ⓐ?.? )</td>
- </tr>
- <tr>
- <td class="nnns top capitalize italic red">
- <br />
- </td>
- <td class="nnns top italic red">
- <br />
- </td>
- <td class="snns top red">item</td>
- <td class="snnn top red">
- <br />
- </td>
- <td class="snnn top red">
- <br />
- </td>
- <td class="ssnn top red">
- <br />
- </td>
- </tr>
- <tr>
- <td class="nnss top capitalize italic red">
- <br />
- </td>
- <td class="snss top italic red">external syntax</td>