- <div xmlns:ld="http://lambdadelta.info/" class="head2">System's Syntax and Behavior</div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">This is a summary of the "block structure"
- of the System's syntactic items and reductions.
- </div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">
- <table cellpadding="4" cellspacing="0">
- <tbody>
- <tr>
- <td class="snns text grey">domain</td>
- <td class="snns plane grey">block</td>
- <td class="snns text grey">leader</td>
- <td class="snns text grey">applicator (with →θ)*</td>
- <td class="snns text grey">reduction</td>
- <td class="snns text grey">→ζ *</td>
- <td class="ssns text grey">reference *</td>
- </tr>
- <tr>
- <td class="snns text">{X | Γ ⊢ X : W}</td>
- <td class="snns plane wine">local typed abstraction *</td>
- <td class="snns text wine">Γ ⊢ +λW</td>
- <td class="snns text wine">ⓐV</td>
- <td class="snns text wine">→β</td>
- <td class="snns text wine">no</td>
- <td class="ssns text wine">#i</td>
- </tr>
- <tr>
- <td class="nnns text">
- <br />
- </td>
- <td class="snns plane magenta">local typed declaration **</td>
- <td class="snns text magenta">Γ ⊢ -λW</td>
- <td class="snns text magenta">ⓐV</td>
- <td class="snns text magenta">→β</td>
- <td class="snns text magenta">no</td>
- <td class="ssns text magenta">#i</td>
- </tr>
- <tr>
- <td class="nnns text">
- <br />
- </td>
- <td class="snns plane prune">global typed declaration ***</td>
- <td class="snns text prune">Γ ⊢ pλW</td>
- <td class="snns text prune">no</td>
- <td class="snns text prune">no</td>
- <td class="snns text prune">no</td>
- <td class="ssns text prune">$p</td>
- </tr>
- <tr>
- <td class="nnns text">
- <br />
- </td>
- <td class="snns plane blue">native type annotation *</td>
- <td class="snns text blue">Γ ⊢ ⓝW</td>
- <td class="snns text blue">no</td>
- <td class="snns text blue">no</td>
- <td class="snns text blue">yes</td>
- <td class="ssns text blue">no</td>
- </tr>
- <tr>
- <td class="snns text">{X | Γ ⊢ X = V}</td>
- <td class="snns plane sky">local abbreviation *</td>
- <td class="snns text sky">Γ ⊢ +δV</td>
- <td class="snns text sky">no</td>
- <td class="snns text sky">local →δ</td>
- <td class="snns text sky">yes</td>
- <td class="ssns text sky">#i</td>
- </tr>
- <tr>
- <td class="nnns text">
- <br />
- </td>
- <td class="snns plane cyan">local definition **</td>
- <td class="snns text cyan">Γ ⊢ -δV</td>
- <td class="snns text cyan">no</td>
- <td class="snns text cyan">local →δ</td>
- <td class="snns text cyan">no</td>
- <td class="ssns text cyan">#i</td>
- </tr>
- <tr>
- <td class="nnns text">
- <br />
- </td>
- <td class="snns plane water">global definition ***</td>
- <td class="snns text water">Γ ⊢ pδV</td>
- <td class="snns text water">no</td>
- <td class="snns text water">global →δ</td>
- <td class="snns text water">no</td>
- <td class="ssns text water">$p</td>
- </tr>
- <tr>
- <td class="snss text">no</td>
- <td class="snss plane green">sort ****</td>
- <td class="snss text green">Γ ⊢ ⋆k</td>
- <td class="snss text green">no</td>
- <td class="snss text green">no</td>
- <td class="snss text green">no</td>
- <td class="ssss text green">no</td>
- </tr>
- </tbody>
- </table>
- </div>
- <div xmlns:ld="http://lambdadelta.info/" class="text">* In terms only.
- ** In terms and local environments only.
- *** In global environments only.
- **** Sort level k in terms only.
- </div>