]> matita.cs.unibo.it Git - helm.git/blob - helm/www/lambdadelta/basic_2.html
update in basic_2
[helm.git] / helm / www / lambdadelta / basic_2.html
1 <?xml version="1.0" encoding="UTF-8"?>
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
3 <html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
4   <head>
5     <meta http-equiv="Content-Language" content="en-us" />
6     <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
7     <meta http-equiv="Content-Style-Type" content="text/css" />
8     <meta name="author" content="Ferruccio Guidi" />
9     <meta name="description" content="lambdadelta version 2" />
10     <title>lambdadelta version 2</title>
11     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
12     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
13     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
14     <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
15   </head>
16   <body lang="en-US">
17     <div class="spacer">
18       <a href="http://lambdadelta.info/">
19         <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
20       </a>
21     </div>
22     <div class="head1">cic:/matita/lambdadelta/basic_2/ (λδ version 2)</div>
23     <div class="spacer">
24       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
25     </div>
26    <div xmlns:ld="http://lambdadelta.info/" class="head2">System's Syntax and Behavior</div>
27    <div xmlns:ld="http://lambdadelta.info/" class="text">This is a summary of the "block structure"
28          of the System's syntactic items and reductions.
29    </div>
30    <div xmlns:ld="http://lambdadelta.info/" class="text">
31       <table cellpadding="4" cellspacing="0">
32         <tbody>
33           <tr>
34             <td class="snns text grey">domain</td>
35             <td class="snns plane grey">block</td>
36             <td class="snns text grey">leader</td>
37             <td class="snns text grey">applicator (with →θ)*</td>
38             <td class="snns text grey">reduction</td>
39             <td class="snns text grey">→ζ *</td>
40             <td class="ssns text grey">reference *</td>
41           </tr>
42           <tr>
43             <td class="snns text">{X | Γ ⊢ X : W}</td>
44             <td class="snns plane wine">local typed abstraction *</td>
45             <td class="snns text wine">Γ ⊢ +λW</td>
46             <td class="snns text wine">ⓐV</td>
47             <td class="snns text wine">→β</td>
48             <td class="snns text wine">no</td>
49             <td class="ssns text wine">#i</td>
50           </tr>
51           <tr>
52             <td class="nnns text">
53               <br />
54             </td>
55             <td class="snns plane magenta">local typed declaration **</td>
56             <td class="snns text magenta">Γ ⊢ -λW</td>
57             <td class="snns text magenta">ⓐV</td>
58             <td class="snns text magenta">→β</td>
59             <td class="snns text magenta">no</td>
60             <td class="ssns text magenta">#i</td>
61           </tr>
62           <tr>
63             <td class="nnns text">
64               <br />
65             </td>
66             <td class="snns plane prune">global typed declaration ***</td>
67             <td class="snns text prune">Γ ⊢ pλW</td>
68             <td class="snns text prune">no</td>
69             <td class="snns text prune">no</td>
70             <td class="snns text prune">no</td>
71             <td class="ssns text prune">$p</td>
72           </tr>
73           <tr>
74             <td class="nnns text">
75               <br />
76             </td>
77             <td class="snns plane blue">native type annotation *</td>
78             <td class="snns text blue">Γ ⊢ ⓝW</td>
79             <td class="snns text blue">no</td>
80             <td class="snns text blue">no</td>
81             <td class="snns text blue">yes</td>
82             <td class="ssns text blue">no</td>
83           </tr>
84           <tr>
85             <td class="snns text">{X | Γ ⊢ X = V}</td>
86             <td class="snns plane sky">local abbreviation *</td>
87             <td class="snns text sky">Γ ⊢ +δV</td>
88             <td class="snns text sky">no</td>
89             <td class="snns text sky">local →δ</td>
90             <td class="snns text sky">yes</td>
91             <td class="ssns text sky">#i</td>
92           </tr>
93           <tr>
94             <td class="nnns text">
95               <br />
96             </td>
97             <td class="snns plane cyan">local definition **</td>
98             <td class="snns text cyan">Γ ⊢ -δV</td>
99             <td class="snns text cyan">no</td>
100             <td class="snns text cyan">local →δ</td>
101             <td class="snns text cyan">no</td>
102             <td class="ssns text cyan">#i</td>
103           </tr>
104           <tr>
105             <td class="nnns text">
106               <br />
107             </td>
108             <td class="snns plane water">global definition ***</td>
109             <td class="snns text water">Γ ⊢ pδV</td>
110             <td class="snns text water">no</td>
111             <td class="snns text water">global →δ</td>
112             <td class="snns text water">no</td>
113             <td class="ssns text water">$p</td>
114           </tr>
115           <tr>
116             <td class="snss text">no</td>
117             <td class="snss plane green">sort ****</td>
118             <td class="snss text green">Γ ⊢ ⋆k</td>
119             <td class="snss text green">no</td>
120             <td class="snss text green">no</td>
121             <td class="snss text green">no</td>
122             <td class="ssss text green">no</td>
123           </tr>
124         </tbody>
125       </table>
126     </div>
127    <div xmlns:ld="http://lambdadelta.info/" class="text">* In terms only.
128          ** In terms and local environments only.
129          *** In global environments only.
130          **** Sort level k in terms only.
131    </div>
132
133    <div xmlns:ld="http://lambdadelta.info/" class="head2">Summary of the Specification</div>
134    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
135          and its timeline.
136    </div>
137    <div xmlns:ld="http://lambdadelta.info/" class="text">
138       <table cellpadding="4" cellspacing="0">
139         <tbody>
140           <tr>
141             <td class="snns component grey">category</td>
142             <td class="snns plane grey">objects</td>
143             <td class="snnn number grey">
144               <br />
145             </td>
146             <td class="snnn plane grey">
147               <br />
148             </td>
149             <td class="snnn number grey">
150               <br />
151             </td>
152             <td class="snnn plane grey">
153               <br />
154             </td>
155             <td class="ssnn number grey">
156               <br />
157             </td>
158           </tr>
159           <tr>
160             <td class="snns component cyan">sizes</td>
161             <td class="snns plane cyan">files</td>
162             <td class="snnn number cyan">173  </td>
163             <td class="snns plane cyan">characters</td>
164             <td class="snnn number cyan">363812</td>
165             <td class="snns plane cyan">nodes</td>
166             <td class="ssnn number cyan">1057233</td>
167           </tr>
168           <tr>
169             <td class="snns component green">propositions</td>
170             <td class="snns plane green">theorems</td>
171             <td class="snnn number green">75</td>
172             <td class="snns plane green">lemmas</td>
173             <td class="snnn number green">750</td>
174             <td class="snns plane green">total</td>
175             <td class="ssnn number green">825</td>
176           </tr>
177           <tr>
178             <td class="snss component yellow">concepts</td>
179             <td class="snss plane yellow">declared</td>
180             <td class="snsn number yellow">43</td>
181             <td class="snss plane yellow">defined</td>
182             <td class="snsn number yellow">68</td>
183             <td class="snss plane yellow">total</td>
184             <td class="sssn number yellow">111</td>
185           </tr>
186         </tbody>
187       </table>
188     </div>
189    <ul xmlns:ld="http://lambdadelta.info/">
190       <li>
191         <span class="date">In progress.</span>
192          Context-sensitive subject equivalence
193          for native type assignment.
194    </li>
195     </ul>
196    <ul xmlns:ld="http://lambdadelta.info/">
197       <li>
198         <span class="date">In progress.</span>
199          Closure of extended context-sensitive computation
200          for native validity.
201    </li>
202     </ul>
203    <ul xmlns:ld="http://lambdadelta.info/">
204       <li>
205         <span class="date">In progress.</span>
206          Extended context-sensitive strong normalization
207          for simply typed terms.
208    </li>
209     </ul>
210    <ul xmlns:ld="http://lambdadelta.info/">
211       <li>
212         <span class="date">2013 April 16.</span>
213          Reaxiomatized substitution and reduction 
214          commute with respect to subclosure
215          (anniversary milestone).
216    </li>
217     </ul>
218    <ul xmlns:ld="http://lambdadelta.info/">
219       <li>
220         <span class="date">2013 March 16.</span>
221          Mutual recursive preservation of stratified native validity
222          for hyper computation on closures.
223    </li>
224     </ul>
225    <ul xmlns:ld="http://lambdadelta.info/">
226       <li>
227         <span class="date">2012 October 16.</span>
228          Confluence for context-free parallel reduction on closures.
229    </li>
230     </ul>
231    <ul xmlns:ld="http://lambdadelta.info/">
232       <li>
233         <span class="date">2012 July 26.</span>
234          Term binders polarized to control ζ reduction.
235    </li>
236     </ul>
237    <ul xmlns:ld="http://lambdadelta.info/">
238       <li>
239         <span class="date">2012 April 16.</span>
240          Context-sensitive subject equivalence
241          for atomic arity assignment
242          (anniversary milestone).
243    </li>
244     </ul>
245    <ul xmlns:ld="http://lambdadelta.info/">
246       <li>
247         <span class="date">2012 March 15.</span>
248          Context-sensitive strong normalization
249          for simply typed terms.
250    </li>
251     </ul>
252    <ul xmlns:ld="http://lambdadelta.info/">
253       <li>
254         <span class="date">2012 January 27.</span>
255          Support for abstract candidates of reducibility.
256    </li>
257     </ul>
258    <ul xmlns:ld="http://lambdadelta.info/">
259       <li>
260         <span class="date">2011 September 21.</span>
261          Confluence for context-sensitive parallel reduction on terms.
262    </li>
263     </ul>
264    <ul xmlns:ld="http://lambdadelta.info/">
265       <li>
266         <span class="date">2011 September 6.</span>
267          Confluence for context-free parallel reduction on terms.
268    </li>
269     </ul>
270    <ul xmlns:ld="http://lambdadelta.info/">
271       <li>
272         <span class="date">2011 April 17.</span>
273          Specification starts.
274    </li>
275     </ul>
276
277    <div xmlns:ld="http://lambdadelta.info/" class="head2">Logical Structure of the Specification</div>
278    <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in planes and components
279          according to the following table.
280          A notation file covering the whole specification is provided.
281          The notation for the relations or functions introduced in each file
282          is shown in parentheses (? are placeholders).
283    </div>
284    <div xmlns:ld="http://lambdadelta.info/" class="text">
285       <table cellpadding="4" cellspacing="0">
286         <tbody>
287           <tr>
288             <td class="snns component grey">component</td>
289             <td class="snns plane grey">plane</td>
290             <td class="snns file grey">files</td>
291             <td class="snnn file grey">
292               <br />
293             </td>
294             <td class="snnn file grey">
295               <br />
296             </td>
297             <td class="ssnn file grey">
298               <br />
299             </td>
300           </tr>
301           <tr>
302             <td class="snns component prune">dynamic typing</td>
303             <td class="snns plane prune">"big tree" parallel computation</td>
304             <td class="snns file prune">yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )</td>
305             <td class="snnn file prune">yprs_yprs</td>
306             <td class="snnn file prune">ygt ( ? ⊢ ⦃?,?⦄ &gt;[g] ⦃?,?⦄ )</td>
307             <td class="ssnn file prune">ygt_ygt</td>
308           </tr>
309           <tr>
310             <td class="nnns component prune">
311               <br />
312             </td>
313             <td class="snns plane prune">"big tree" parallel reduction</td>
314             <td class="snns file prune">ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )</td>
315             <td class="snnn file prune">ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )</td>
316             <td class="snnn file prune">
317               <br />
318             </td>
319             <td class="ssnn file prune">
320               <br />
321             </td>
322           </tr>
323           <tr>
324             <td class="nnns component prune">
325               <br />
326             </td>
327             <td class="snns plane prune">local env. ref. for stratified native validity</td>
328             <td class="snns file prune">lsubsv ( ? ⊢ ? ¡⊑[?] ? )</td>
329             <td class="snnn file prune">lsubsv_ldrop lsubsv_lsuba lsubsv_ssta lsubsv_dxprs lsubsv_cpcs lsubsv_snv</td>
330             <td class="snnn file prune">
331               <br />
332             </td>
333             <td class="ssnn file prune">
334               <br />
335             </td>
336           </tr>
337           <tr>
338             <td class="nnns component prune">
339               <br />
340             </td>
341             <td class="snns plane prune">stratified native validity</td>
342             <td class="snns file prune">snv ( ⦃?,?⦄ ⊢ ? ¡[?] )</td>
343             <td class="snnn file prune">snv_lift snv_lpss snv_aaa snv_ssta snv_sstas snv_ssta_lpr snv_lpr snv_cpcs</td>
344             <td class="snnn file prune">
345               <br />
346             </td>
347             <td class="ssnn file prune">
348               <br />
349             </td>
350           </tr>
351           <tr>
352             <td class="snns component blue">equivalence</td>
353             <td class="snns plane blue">local env. ref. for stratified static type assignment</td>
354             <td class="snns file blue">lsubss ( ? •⊑[?] ? )</td>
355             <td class="snnn file blue">lsubss_ldrop lsubss_ssta lsubss_cpcs</td>
356             <td class="snnn file blue">
357               <br />
358             </td>
359             <td class="ssnn file blue">
360               <br />
361             </td>
362           </tr>
363           <tr>
364             <td class="nnns component blue">
365               <br />
366             </td>
367             <td class="snns plane blue">context-sensitive equivalence</td>
368             <td class="snns file blue">cpcs ( ? ⊢ ? ⬌* ? )</td>
369             <td class="snnn file blue">cpcs_lpss cpcs_aaa cpcs_cprs cpcs_cpcs</td>
370             <td class="snnn file blue">
371               <br />
372             </td>
373             <td class="ssnn file blue">
374               <br />
375             </td>
376           </tr>
377           <tr>
378             <td class="snns component sky">conversion</td>
379             <td class="snns plane sky">context-sensitive conversion</td>
380             <td class="snns file sky">cpc ( ? ⊢ ? ⬌ ? )</td>
381             <td class="snnn file sky">cpc_cpc</td>
382             <td class="snnn file sky">
383               <br />
384             </td>
385             <td class="ssnn file sky">
386               <br />
387             </td>
388           </tr>
389           <tr>
390             <td class="snns component cyan">computation</td>
391             <td class="snns plane cyan">decomposed extended computation</td>
392             <td class="snns file cyan">dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )</td>
393             <td class="snnn file cyan">dxprs_lift dxprs_lpss dxprs_aaa dxprs_dxprs</td>
394             <td class="snnn file cyan">
395               <br />
396             </td>
397             <td class="ssnn file cyan">
398               <br />
399             </td>
400           </tr>
401           <tr>
402             <td class="nnns component cyan">
403               <br />
404             </td>
405             <td class="snns plane cyan">weakly normalizing computation</td>
406             <td class="snns file cyan">cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )</td>
407             <td class="snnn file cyan">cpe_cpe</td>
408             <td class="snnn file cyan">
409               <br />
410             </td>
411             <td class="ssnn file cyan">
412               <br />
413             </td>
414           </tr>
415           <tr>
416             <td class="nnns component cyan">
417               <br />
418             </td>
419             <td class="snns plane cyan">strongly normalizing computation</td>
420             <td class="snns file cyan">csn_vector ( ? ⊢ ⬊* ? )</td>
421             <td class="snnn file cyan">csn_tstc_vector csn_aaa</td>
422             <td class="snnn file cyan">
423               <br />
424             </td>
425             <td class="ssnn file cyan">
426               <br />
427             </td>
428           </tr>
429           <tr>
430             <td class="nnns component cyan">
431               <br />
432             </td>
433             <td class="nnns plane cyan">
434               <br />
435             </td>
436             <td class="snns file cyan">csn ( ? ⊢ ⬊* ? )</td>
437             <td class="snnn file cyan">csn_alt ( ? ⊢ ⬊⬊* ? )</td>
438             <td class="snnn file cyan">csn_lift csn_lpr</td>
439             <td class="ssnn file cyan">
440               <br />
441             </td>
442           </tr>
443           <tr>
444             <td class="nnns component cyan">
445               <br />
446             </td>
447             <td class="snns plane cyan">context-sensitive computation</td>
448             <td class="snns file cyan">lprs ( ? ⊢ ➡* ? )</td>
449             <td class="snnn file cyan">lprs_alt ( ? ⊢ ➡➡* ? )</td>
450             <td class="snnn file cyan">lprs_ldrop lprs_lpss lprs_aaa lprs_cprs lprs_lprs</td>
451             <td class="ssnn file cyan">
452               <br />
453             </td>
454           </tr>
455           <tr>
456             <td class="nnns component cyan">
457               <br />
458             </td>
459             <td class="nnns plane cyan">
460               <br />
461             </td>
462             <td class="snns file cyan">cprs ( ? ⊢ ? ➡* ?)</td>
463             <td class="snnn file cyan">cprs_tstc cprs_tstc_vector cprs_lift cprs_lpss cprs_aaa cprs_cprs</td>
464             <td class="snnn file cyan">
465               <br />
466             </td>
467             <td class="ssnn file cyan">
468               <br />
469             </td>
470           </tr>
471           <tr>
472             <td class="nnns component cyan">
473               <br />
474             </td>
475             <td class="snns plane cyan">local env. ref. for abstract candidates of reducibility</td>
476             <td class="snns file cyan">lsubc ( ? ⊑[?] ? )</td>
477             <td class="snnn file cyan">lsubc_ldrop lsubc_ldrops lsubc_lsuba</td>
478             <td class="snnn file cyan">
479               <br />
480             </td>
481             <td class="ssnn file cyan">
482               <br />
483             </td>
484           </tr>
485           <tr>
486             <td class="nnns component cyan">
487               <br />
488             </td>
489             <td class="snns plane cyan">support for abstract computation properties</td>
490             <td class="snns file cyan">acp</td>
491             <td class="snnn file cyan">acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )</td>
492             <td class="snnn file cyan">acp_aaa</td>
493             <td class="ssnn file cyan">
494               <br />
495             </td>
496           </tr>
497           <tr>
498             <td class="snns component water">reduction</td>
499             <td class="snns plane water">context-sensitive extended reduction</td>
500             <td class="snns file water">lpx ( ⦃?,?⦄ ⊢ ➡[?] ? )</td>
501             <td class="snnn file water">lpx_ldrop lpx_aaa</td>
502             <td class="snnn file water">
503               <br />
504             </td>
505             <td class="ssnn file water">
506               <br />
507             </td>
508           </tr>
509           <tr>
510             <td class="nnns component water">
511               <br />
512             </td>
513             <td class="nnns plane water">
514               <br />
515             </td>
516             <td class="snns file water">cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? )</td>
517             <td class="snnn file water">cpx_lift</td>
518             <td class="snnn file water">
519               <br />
520             </td>
521             <td class="ssnn file water">
522               <br />
523             </td>
524           </tr>
525           <tr>
526             <td class="nnns component water">
527               <br />
528             </td>
529             <td class="snns plane water">context-sensitive normal forms</td>
530             <td class="snns file water">cnf ( ? ⊢ 𝐍⦃?⦄ )</td>
531             <td class="snnn file water">cnf_liftt cnf_crf cnf_cif</td>
532             <td class="snnn file water">
533               <br />
534             </td>
535             <td class="ssnn file water">
536               <br />
537             </td>
538           </tr>
539           <tr>
540             <td class="nnns component water">
541               <br />
542             </td>
543             <td class="snns plane water">context-sensitive reduction</td>
544             <td class="snns file water">lpr ( ? ⊢ ➡ ? )</td>
545             <td class="snnn file water">lpr_ldrop lpr_lpss lpr_lpr</td>
546             <td class="snnn file water">
547               <br />
548             </td>
549             <td class="ssnn file water">
550               <br />
551             </td>
552           </tr>
553           <tr>
554             <td class="nnns component water">
555               <br />
556             </td>
557             <td class="nnns plane water">
558               <br />
559             </td>
560             <td class="snns file water">cpr ( ? ⊢ ? ➡ ? )</td>
561             <td class="snnn file water">cpr_lift cpr_cif</td>
562             <td class="snnn file water">
563               <br />
564             </td>
565             <td class="ssnn file water">
566               <br />
567             </td>
568           </tr>
569           <tr>
570             <td class="nnns component water">
571               <br />
572             </td>
573             <td class="snns plane water">context-sensitive reducible forms</td>
574             <td class="snns file water">crf ( ? ⊢ 𝐑⦃?⦄ )</td>
575             <td class="snnn file water">crf_append</td>
576             <td class="snnn file water">cif ( ? ⊢ 𝐈⦃?⦄ )</td>
577             <td class="ssnn file water">cif_append</td>
578           </tr>
579           <tr>
580             <td class="snns component green">unfold</td>
581             <td class="snns plane green">restricted parallel computation</td>
582             <td class="snns file green">lpqs ( ? ⊢ ➤* ? )</td>
583             <td class="snnn file green">lpqs_ldrop lpqs_cpqs lpqs_lpqs</td>
584             <td class="snnn file green">
585               <br />
586             </td>
587             <td class="ssnn file green">
588               <br />
589             </td>
590           </tr>
591           <tr>
592             <td class="nnns component green">
593               <br />
594             </td>
595             <td class="nnns plane green">
596               <br />
597             </td>
598             <td class="snns file green">cpqs ( ? ⊢ ? ➤* ? )</td>
599             <td class="snnn file green">cpqs_lift</td>
600             <td class="snnn file green">
601               <br />
602             </td>
603             <td class="ssnn file green">
604               <br />
605             </td>
606           </tr>
607           <tr>
608             <td class="nnns component green">
609               <br />
610             </td>
611             <td class="snns plane green">unfold</td>
612             <td class="snns file green">unfold ( ? ⊢ ? ⧫* ? )</td>
613             <td class="snnn file green">
614               <br />
615             </td>
616             <td class="snnn file green">
617               <br />
618             </td>
619             <td class="ssnn file green">
620               <br />
621             </td>
622           </tr>
623           <tr>
624             <td class="nnns component green">
625               <br />
626             </td>
627             <td class="snns plane green">iterated stratified static type assignment</td>
628             <td class="snns file green">sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )</td>
629             <td class="snnn file green">sstas_lift sstas_lpss sstas_aaa sstas_sstas</td>
630             <td class="snnn file green">
631               <br />
632             </td>
633             <td class="ssnn file green">
634               <br />
635             </td>
636           </tr>
637           <tr>
638             <td class="snns component grass">static typing</td>
639             <td class="snns plane grass">stratified static type assignment</td>
640             <td class="snns file grass">ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )</td>
641             <td class="snnn file grass">ssta_lift ssta_lpss ssta_aaa ssta_ssta</td>
642             <td class="snnn file grass">
643               <br />
644             </td>
645             <td class="ssnn file grass">
646               <br />
647             </td>
648           </tr>
649           <tr>
650             <td class="nnns component grass">
651               <br />
652             </td>
653             <td class="snns plane grass">local env. ref. for atomic arity assignment</td>
654             <td class="snns file grass">lsuba ( ? ⁝⊑ ? )</td>
655             <td class="snnn file grass">lsuba_ldrop lsuba_aaa lsuba_lsuba</td>
656             <td class="snnn file grass">
657               <br />
658             </td>
659             <td class="ssnn file grass">
660               <br />
661             </td>
662           </tr>
663           <tr>
664             <td class="nnns component grass">
665               <br />
666             </td>
667             <td class="snns plane grass">atomic arity assignment</td>
668             <td class="snns file grass">aaa ( ? ⊢ ? ⁝ ? )</td>
669             <td class="snnn file grass">aaa_lift aaa_lifts aaa_lpss aaa_aaa</td>
670             <td class="snnn file grass">
671               <br />
672             </td>
673             <td class="ssnn file grass">
674               <br />
675             </td>
676           </tr>
677           <tr>
678             <td class="nnns component grass">
679               <br />
680             </td>
681             <td class="snns plane grass">parameters</td>
682             <td class="snns file grass">sh</td>
683             <td class="snnn file grass">sd</td>
684             <td class="snnn file grass">
685               <br />
686             </td>
687             <td class="ssnn file grass">
688               <br />
689             </td>
690           </tr>
691           <tr>
692             <td class="snns component yellow">substitution</td>
693             <td class="snns plane yellow">parallel substitution</td>
694             <td class="snns file yellow">lpss ( ? ⊢ ▶* ? )</td>
695             <td class="snnn file yellow">lpss_ldrop lpss_cpss lpss_lpss</td>
696             <td class="snnn file yellow">
697               <br />
698             </td>
699             <td class="ssnn file yellow">
700               <br />
701             </td>
702           </tr>
703           <tr>
704             <td class="nnns component yellow">
705               <br />
706             </td>
707             <td class="nnns plane yellow">
708               <br />
709             </td>
710             <td class="snns file yellow">cpss ( ? ⊢ ? ▶* ? )</td>
711             <td class="snnn file yellow">cpss_lift</td>
712             <td class="snnn file yellow">
713               <br />
714             </td>
715             <td class="ssnn file yellow">
716               <br />
717             </td>
718           </tr>
719           <tr>
720             <td class="nnns component yellow">
721               <br />
722             </td>
723             <td class="snns plane yellow">local env. ref. for substitution</td>
724             <td class="snns file yellow">lsubr ( ? ⊑ ? )</td>
725             <td class="snnn file yellow">lsubr_lsubr</td>
726             <td class="snnn file yellow">
727               <br />
728             </td>
729             <td class="ssnn file yellow">
730               <br />
731             </td>
732           </tr>
733           <tr>
734             <td class="nnns component yellow">
735               <br />
736             </td>
737             <td class="snns plane yellow">iterated structural successor for closures</td>
738             <td class="snns file yellow">fsups ( ⦃?,?⦄ ⊃* ⦃?,?⦄ )</td>
739             <td class="snnn file yellow">fsups_fsups</td>
740             <td class="snnn file yellow">
741               <br />
742             </td>
743             <td class="ssnn file yellow">
744               <br />
745             </td>
746           </tr>
747           <tr>
748             <td class="nnns component yellow">
749               <br />
750             </td>
751             <td class="nnns plane yellow">
752               <br />
753             </td>
754             <td class="snns file yellow">fsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ )</td>
755             <td class="snnn file yellow">fsupp_fsupp</td>
756             <td class="snnn file yellow">
757               <br />
758             </td>
759             <td class="ssnn file yellow">
760               <br />
761             </td>
762           </tr>
763           <tr>
764             <td class="nnns component yellow">
765               <br />
766             </td>
767             <td class="snns plane yellow">generic local env. slicing</td>
768             <td class="snns file yellow">ldrops ( ⇩*[?] ? ≡ ? )</td>
769             <td class="snnn file yellow">ldrops_ldrop ldrops_ldrops</td>
770             <td class="snnn file yellow">
771               <br />
772             </td>
773             <td class="ssnn file yellow">
774               <br />
775             </td>
776           </tr>
777           <tr>
778             <td class="nnns component yellow">
779               <br />
780             </td>
781             <td class="snns plane yellow">generic term relocation</td>
782             <td class="snns file yellow">lifts_vector ( ⇧*[?] ? ≡ ? )</td>
783             <td class="snnn file yellow">lifts_lift_vector</td>
784             <td class="snnn file yellow">
785               <br />
786             </td>
787             <td class="ssnn file yellow">
788               <br />
789             </td>
790           </tr>
791           <tr>
792             <td class="nnns component yellow">
793               <br />
794             </td>
795             <td class="nnns plane yellow">
796               <br />
797             </td>
798             <td class="snns file yellow">lifts ( ⇧*[?] ? ≡ ? )</td>
799             <td class="snnn file yellow">lifts_lift lifts_lifts</td>
800             <td class="snnn file yellow">
801               <br />
802             </td>
803             <td class="ssnn file yellow">
804               <br />
805             </td>
806           </tr>
807           <tr>
808             <td class="nnns component yellow">
809               <br />
810             </td>
811             <td class="snns plane yellow">support for generic relocation</td>
812             <td class="snns file yellow">gr2 ( @⦃?,?⦄ ≡ ? )</td>
813             <td class="snnn file yellow">gr2_plus ( ? + ? )</td>
814             <td class="snnn file yellow">gr2_minus ( ? ▭ ? ≡ ? )</td>
815             <td class="ssnn file yellow">gr2_gr2</td>
816           </tr>
817           <tr>
818             <td class="snns component orange">relocation</td>
819             <td class="snns plane orange">structural successor for closures</td>
820             <td class="snns file orange">fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ )</td>
821             <td class="snnn file orange">fsupq ( ⦃?,?⦄ ⊃⸮ ⦃?,?⦄ )</td>
822             <td class="snnn file orange">
823               <br />
824             </td>
825             <td class="ssnn file orange">
826               <br />
827             </td>
828           </tr>
829           <tr>
830             <td class="nnns component orange">
831               <br />
832             </td>
833             <td class="snns plane orange">global env. slicing</td>
834             <td class="snns file orange">gdrop ( ⇩[?] ? ≡ ? )</td>
835             <td class="snnn file orange">gdrop_gdrop</td>
836             <td class="snnn file orange">
837               <br />
838             </td>
839             <td class="ssnn file orange">
840               <br />
841             </td>
842           </tr>
843           <tr>
844             <td class="nnns component orange">
845               <br />
846             </td>
847             <td class="snns plane orange">basic local env. slicing</td>
848             <td class="snns file orange">ldrop ( ⇩[?,?] ? ≡ ? )</td>
849             <td class="snnn file orange">ldrop_append ldrop_lpx_sn ldrop_ldrop</td>
850             <td class="snnn file orange">
851               <br />
852             </td>
853             <td class="ssnn file orange">
854               <br />
855             </td>
856           </tr>
857           <tr>
858             <td class="nnns component orange">
859               <br />
860             </td>
861             <td class="snns plane orange">basic term relocation</td>
862             <td class="snns file orange">lift_vector ( ⇧[?,?] ? ≡ ? )</td>
863             <td class="snnn file orange">lift_lift_vector</td>
864             <td class="snnn file orange">
865               <br />
866             </td>
867             <td class="ssnn file orange">
868               <br />
869             </td>
870           </tr>
871           <tr>
872             <td class="nnns component orange">
873               <br />
874             </td>
875             <td class="nnns plane orange">
876               <br />
877             </td>
878             <td class="snns file orange">lift ( ⇧[?,?] ? ≡ ? )</td>
879             <td class="snnn file orange">lift_lift</td>
880             <td class="snnn file orange">
881               <br />
882             </td>
883             <td class="ssnn file orange">
884               <br />
885             </td>
886           </tr>
887           <tr>
888             <td class="snns component red">grammar</td>
889             <td class="snns plane red">pointwise extension of a relation</td>
890             <td class="snns file red">lpx_sn</td>
891             <td class="snnn file red">lpx_sn_tc lpx_sn_lpx_sn</td>
892             <td class="snnn file red">
893               <br />
894             </td>
895             <td class="ssnn file red">
896               <br />
897             </td>
898           </tr>
899           <tr>
900             <td class="nnns component red">
901               <br />
902             </td>
903             <td class="snns plane red">same top term constructor</td>
904             <td class="snns file red">tstc ( ? ≃ ? )</td>
905             <td class="snnn file red">tstc_tstc tstc_vector</td>
906             <td class="snnn file red">
907               <br />
908             </td>
909             <td class="ssnn file red">
910               <br />
911             </td>
912           </tr>
913           <tr>
914             <td class="nnns component red">
915               <br />
916             </td>
917             <td class="snns plane red">closures</td>
918             <td class="snns file red">cl_shift ( ? @@ ? )</td>
919             <td class="snnn file red">cl_weight ( ♯{?,?} )</td>
920             <td class="snnn file red">
921               <br />
922             </td>
923             <td class="ssnn file red">
924               <br />
925             </td>
926           </tr>
927           <tr>
928             <td class="nnns component red">
929               <br />
930             </td>
931             <td class="snns plane red">internal syntax</td>
932             <td class="snns file red">genv</td>
933             <td class="snnn file red">
934               <br />
935             </td>
936             <td class="snnn file red">
937               <br />
938             </td>
939             <td class="ssnn file red">
940               <br />
941             </td>
942           </tr>
943           <tr>
944             <td class="nnns component red">
945               <br />
946             </td>
947             <td class="nnns plane red">
948               <br />
949             </td>
950             <td class="snns file red">lenv</td>
951             <td class="snnn file red">lenv_weight ( ♯{?} )</td>
952             <td class="snnn file red">lenv_length ( |?| )</td>
953             <td class="ssnn file red">lenv_append ( ? @@ ? )</td>
954           </tr>
955           <tr>
956             <td class="nnns component red">
957               <br />
958             </td>
959             <td class="nnns plane red">
960               <br />
961             </td>
962             <td class="snns file red">term</td>
963             <td class="snnn file red">term_weight ( ♯{?} )</td>
964             <td class="snnn file red">term_simple ( 𝐒⦃?⦄ )</td>
965             <td class="ssnn file red">term_vector</td>
966           </tr>
967           <tr>
968             <td class="nnns component red">
969               <br />
970             </td>
971             <td class="nnns plane red">
972               <br />
973             </td>
974             <td class="snns file red">item</td>
975             <td class="snnn file red">
976               <br />
977             </td>
978             <td class="snnn file red">
979               <br />
980             </td>
981             <td class="ssnn file red">
982               <br />
983             </td>
984           </tr>
985           <tr>
986             <td class="nnss component red">
987               <br />
988             </td>
989             <td class="snss plane red">external syntax</td>
990             <td class="snss file red">aarity</td>
991             <td class="snsn file red">
992               <br />
993             </td>
994             <td class="snsn file red">
995               <br />
996             </td>
997             <td class="sssn file red">
998               <br />
999             </td>
1000           </tr>
1001         </tbody>
1002       </table>
1003     </div>
1004
1005    <div xmlns:ld="http://lambdadelta.info/" class="head2">Physical Structure of the Specification</div>
1006    <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in directories,
1007          one for each component.
1008    </div>
1009    <div class="spacer">
1010       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
1011     </div>
1012     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
1013       <br />
1014     </div>
1015     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
1016       <a href="http://validator.w3.org/check?uri=referer">
1017         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
1018       </a>
1019       <a href="http://jigsaw.w3.org/css-validator/check/referer">
1020         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
1021       </a>
1022       <a href="http://www.w3.org/XML/">
1023         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
1024       </a>
1025       <a href="http://www.w3.org/Graphics/PNG/">
1026         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
1027       </a>
1028       <a href="http://www.anybrowser.org/campaign/">
1029         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
1030       </a>
1031     </div>
1032     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
1033       <br />
1034     </div>
1035     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 08 Jun 2013 22:22:33 +0200</div>
1036 </body>
1037 </html>