]> matita.cs.unibo.it Git - helm.git/blob - helm/www/lambdadelta/basic_2.html
update in basic_2 and apps_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="\lambda\delta home page" />
10     <title>\lambda\delta home page</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/ (core λδ 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="spacer">
27       <br />
28     </div>
29     <div xmlns:ld="http://lambdadelta.info/" class="text">
30       <table cellpadding="4" cellspacing="0">
31         <tbody>
32           <tr>
33             <td class="snns capitalize italic sky">
34               <a href="http://lambdadelta.info/index.html">home</a>
35             </td>
36             <td class="snns capitalize italic magenta">
37               <a href="http://lambdadelta.info/news.html">news</a>
38             </td>
39             <td class="snns capitalize italic white">
40               <a href="http://lambdadelta.info/specification.html">specification</a>
41             </td>
42             <td class="snnn capitalize italic white">
43               <br />
44             </td>
45             <td class="snnn capitalize italic white">
46               <br />
47             </td>
48             <td class="snns capitalize italic orange">
49               <a href="http://lambdadelta.info/documentation.html">documentation</a>
50             </td>
51             <td class="snns capitalize italic green">
52               <a href="http://lambdadelta.info/implementation.html">implementation</a>
53             </td>
54             <td class="ssnn capitalize italic green">
55               <br />
56             </td>
57           </tr>
58           <tr>
59             <td class="snns capitalize sky">
60               <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
61             </td>
62             <td class="snns capitalize magenta">
63               <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
64             </td>
65             <td class="snns capitalize white">
66               <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
67             </td>
68             <td class="snnn capitalize white">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
69             <td class="snnn capitalize white">
70               <br />
71             </td>
72             <td class="snns capitalize orange">
73               <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
74             </td>
75             <td class="snns capitalize green">
76               <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
77             </td>
78             <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
79           </tr>
80           <tr>
81             <td class="snss capitalize sky">
82               <a href="http://lambdadelta.info/index.html#citations">citations</a>
83             </td>
84             <td class="snss capitalize magenta">
85               <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
86             </td>
87             <td class="snss capitalize white">
88               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
89             </td>
90             <td class="snsn capitalize white">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
91             <td class="snsn capitalize white">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
92             <td class="snss capitalize orange">
93               <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
94             </td>
95             <td class="snss capitalize green">
96               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
97             </td>
98             <td class="sssn capitalize green">
99               <br />
100             </td>
101           </tr>
102         </tbody>
103       </table>
104     </div>
105     <!--   
106    <section>System's Syntax and Behavior</section>
107    <body>This is a summary of the "block structure"
108          of the System's syntactic items and reductions.
109    </body>
110    <table name="basic_2_blk"/>
111    <body>* In terms only.
112          ** In terms and local environments only.
113          *** In global environments only.
114          **** Sort level k in terms only.
115    </body>
116 -->
117     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
118     </div>
119     <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical account of the specification's contents
120          and its timeline.
121    </div>
122     <div xmlns:ld="http://lambdadelta.info/" class="text">
123       <table cellpadding="4" cellspacing="0">
124         <tbody>
125           <tr>
126             <td class="snns capitalize italic gray">category</td>
127             <td class="snns italic gray">objects</td>
128             <td class="snnn right italic gray">
129               <br />
130             </td>
131             <td class="snnn italic gray">
132               <br />
133             </td>
134             <td class="snnn right italic gray">
135               <br />
136             </td>
137             <td class="snnn italic gray">
138               <br />
139             </td>
140             <td class="ssnn right italic gray">
141               <br />
142             </td>
143           </tr>
144           <tr>
145             <td class="snns capitalize italic cyan">sizes</td>
146             <td class="snns italic cyan">files</td>
147             <td class="snnn right italic cyan">83</td>
148             <td class="snns italic cyan">characters</td>
149             <td class="snnn right italic cyan">55955</td>
150             <td class="snns italic cyan">nodes</td>
151             <td class="ssnn right italic cyan">191279</td>
152           </tr>
153           <tr>
154             <td class="snns capitalize italic green">propositions</td>
155             <td class="snns italic green">theorems</td>
156             <td class="snnn right italic green">33</td>
157             <td class="snns italic green">lemmas</td>
158             <td class="snnn right italic green">211</td>
159             <td class="snns italic green">total</td>
160             <td class="ssnn right italic green">244</td>
161           </tr>
162           <tr>
163             <td class="snss capitalize italic yellow">concepts</td>
164             <td class="snss italic yellow">declared</td>
165             <td class="snsn right italic yellow">15</td>
166             <td class="snss italic yellow">defined</td>
167             <td class="snsn right italic yellow">23</td>
168             <td class="snss italic yellow">total</td>
169             <td class="sssn right italic yellow">38</td>
170           </tr>
171         </tbody>
172       </table>
173     </div>
174     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="B">Stage "B"</div>
175     <ul xmlns:ld="http://lambdadelta.info/">
176       <li>
177         <span class="emph alpha">Ongoing.</span>
178          Context-sensitive subject equivalence
179          for native type assignment.
180    </li>
181     </ul>
182     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="A2">Stage "A2": "Extending the Applicability Condition"</div>
183     <ul xmlns:ld="http://lambdadelta.info/">
184       <li>
185         <span class="emph alpha">2015 October 9.</span>
186          λδ version 2A2 is started.
187    </li>
188     </ul>
189     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="A1">Stage "A1": "Extending the Applicability Condition"</div>
190     <ul xmlns:ld="http://lambdadelta.info/">
191       <li>
192         <span class="emph delta">2015 August 27.</span>
193          λδ version 2A1 appears too complex and is dismissed.
194    </li>
195     </ul>
196     <ul xmlns:ld="http://lambdadelta.info/">
197       <li>
198         <span class="emph gamma">2014 October 28.</span>
199          λδ version 2A1 is released.
200    </li>
201     </ul>
202     <ul xmlns:ld="http://lambdadelta.info/">
203       <li>
204         <span class="emph beta">2014 September 9.</span>
205          Iterated static type assignment defined (more elegantly)
206          as a primitive notion.
207    </li>
208     </ul>
209     <ul xmlns:ld="http://lambdadelta.info/">
210       <li>
211         <span class="emph beta">2014 June 18.</span>
212          Preservation of stratified native validity
213          for context-sensitive computation on terms.
214    </li>
215     </ul>
216     <ul xmlns:ld="http://lambdadelta.info/">
217       <li>
218         <span class="emph alpha">2014 June 9.</span>
219          Strong qrst-normalization
220          for simply typed terms.
221    </li>
222     </ul>
223     <ul xmlns:ld="http://lambdadelta.info/">
224       <li>
225         <span class="emph alpha">2014 April 16.</span>
226          Lazy equivalence on local environments
227          added as q-step to rst-computation on closures
228          (anniversary milestone).
229    </li>
230     </ul>
231     <ul xmlns:ld="http://lambdadelta.info/">
232       <li>
233         <span class="emph alpha">2014 January 20.</span>
234          Parametrized slicing of local environments
235          comprises both versions of this operation
236          (one from basic_1, the other used in basic_2 till now).
237    </li>
238     </ul>
239     <ul xmlns:ld="http://lambdadelta.info/">
240       <li>
241         <span class="emph alpha">2013 August 7.</span>
242          Passive support for global environments.
243    </li>
244     </ul>
245     <ul xmlns:ld="http://lambdadelta.info/">
246       <li>
247         <span class="emph alpha">2013 July 27.</span>
248          Reaxiomatized β-reductum as in rt-reduction.
249    </li>
250     </ul>
251     <ul xmlns:ld="http://lambdadelta.info/">
252       <li>
253         <span class="emph alpha">2013 July 20.</span>
254          Context-sensitive strong rt-normalization
255          for simply typed terms.
256    </li>
257     </ul>
258     <ul xmlns:ld="http://lambdadelta.info/">
259       <li>
260         <span class="emph alpha">2013 April 16.</span>
261          Reaxiomatized substitution and reduction
262          commute with respect to subclosure
263          (anniversary milestone).
264    </li>
265     </ul>
266     <ul xmlns:ld="http://lambdadelta.info/">
267       <li>
268         <span class="emph alpha">2013 March 16.</span>
269          Mutual recursive preservation of stratified native validity
270          for rst-computation on closures.
271    </li>
272     </ul>
273     <ul xmlns:ld="http://lambdadelta.info/">
274       <li>
275         <span class="emph alpha">2012 October 16.</span>
276          Confluence for context-free parallel reduction on closures.
277    </li>
278     </ul>
279     <ul xmlns:ld="http://lambdadelta.info/">
280       <li>
281         <span class="emph alpha">2012 July 26.</span>
282          Term binders polarized to control ζ-reduction (not released).
283    </li>
284     </ul>
285     <ul xmlns:ld="http://lambdadelta.info/">
286       <li>
287         <span class="emph alpha">2012 April 16.</span>
288          Context-sensitive subject equivalence
289          for atomic arity assignment
290          (anniversary milestone).
291    </li>
292     </ul>
293     <ul xmlns:ld="http://lambdadelta.info/">
294       <li>
295         <span class="emph alpha">2012 March 15.</span>
296          Context-sensitive strong normalization
297          for simply typed terms.
298    </li>
299     </ul>
300     <ul xmlns:ld="http://lambdadelta.info/">
301       <li>
302         <span class="emph alpha">2012 January 27.</span>
303          Support for abstract candidates of reducibility.
304    </li>
305     </ul>
306     <ul xmlns:ld="http://lambdadelta.info/">
307       <li>
308         <span class="emph alpha">2011 September 21.</span>
309          Confluence for context-sensitive parallel reduction on terms.
310    </li>
311     </ul>
312     <ul xmlns:ld="http://lambdadelta.info/">
313       <li>
314         <span class="emph alpha">2011 September 6.</span>
315          Confluence for context-free parallel reduction on terms.
316    </li>
317     </ul>
318     <ul xmlns:ld="http://lambdadelta.info/">
319       <li>
320         <span class="emph alpha">2011 April 17.</span>
321          λδ version 2 is started.
322    </li>
323     </ul>
324     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
325     </div>
326     <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
327    </div>
328     <div xmlns:ld="http://lambdadelta.info/" class="text">
329       <table cellpadding="4" cellspacing="0">
330         <tbody>
331           <tr>
332             <td class="snns top capitalize italic gray">component</td>
333             <td class="snns top italic gray">plane</td>
334             <td class="snns top gray">files</td>
335             <td class="snnn top gray">
336               <br />
337             </td>
338             <td class="snnn top gray">
339               <br />
340             </td>
341             <td class="ssnn top gray">
342               <br />
343             </td>
344           </tr>
345           <tr>
346             <td class="snns top capitalize italic yellow">relocation</td>
347             <td class="snns top italic yellow">ranged equivalence for closures</td>
348             <td class="snns top yellow">freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )</td>
349             <td class="snnn top yellow">freq_freq</td>
350             <td class="snnn top yellow">
351               <br />
352             </td>
353             <td class="ssnn top yellow">
354               <br />
355             </td>
356           </tr>
357           <tr>
358             <td class="nnns top capitalize italic yellow">
359               <br />
360             </td>
361             <td class="snns top italic yellow">context-sensitive free variables</td>
362             <td class="snns top yellow">frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )</td>
363             <td class="snnn top yellow">frees_weight frees_lreq frees_frees</td>
364             <td class="snnn top yellow">
365               <br />
366             </td>
367             <td class="ssnn top yellow">
368               <br />
369             </td>
370           </tr>
371           <tr>
372             <td class="nnns top capitalize italic yellow">
373               <br />
374             </td>
375             <td class="snns top italic yellow">generic slicing for local environments</td>
376             <td class="snns top yellow">drops_vector ( ⬇*[?,?] ? ≡ ? )</td>
377             <td class="snnn top yellow">
378               <br />
379             </td>
380             <td class="snnn top yellow">
381               <br />
382             </td>
383             <td class="ssnn top yellow">
384               <br />
385             </td>
386           </tr>
387           <tr>
388             <td class="nnns top capitalize italic yellow">
389               <br />
390             </td>
391             <td class="nnns top italic yellow">
392               <br />
393             </td>
394             <td class="snns top yellow">drops ( ⬇*[?,?] ? ≡ ? )</td>
395             <td class="snnn top yellow">drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops</td>
396             <td class="snnn top yellow">
397               <br />
398             </td>
399             <td class="ssnn top yellow">
400               <br />
401             </td>
402           </tr>
403           <tr>
404             <td class="nnns top capitalize italic yellow">
405               <br />
406             </td>
407             <td class="snns top italic yellow">generic relocation for terms</td>
408             <td class="snns top yellow">lifts_vector ( ⬆*[?] ? ≡ ? )</td>
409             <td class="snnn top yellow">lifts_lift_vector</td>
410             <td class="snnn top yellow">
411               <br />
412             </td>
413             <td class="ssnn top yellow">
414               <br />
415             </td>
416           </tr>
417           <tr>
418             <td class="nnns top capitalize italic yellow">
419               <br />
420             </td>
421             <td class="nnns top italic yellow">
422               <br />
423             </td>
424             <td class="snns top yellow">lifts ( ⬆*[?] ? ≡ ? )</td>
425             <td class="snnn top yellow">lifts_simple lifts_weight lifts_lifts</td>
426             <td class="snnn top yellow">
427               <br />
428             </td>
429             <td class="ssnn top yellow">
430               <br />
431             </td>
432           </tr>
433           <tr>
434             <td class="nnns top capitalize italic yellow">
435               <br />
436             </td>
437             <td class="snns top italic yellow">ranged equivalence for local environments</td>
438             <td class="snns top yellow">lreq ( ? ≡[?] ? )</td>
439             <td class="snnn top yellow">lreq_length lreq_lreq</td>
440             <td class="snnn top yellow">
441               <br />
442             </td>
443             <td class="ssnn top yellow">
444               <br />
445             </td>
446           </tr>
447           <tr>
448             <td class="nnns top capitalize italic yellow">
449               <br />
450             </td>
451             <td class="snns top italic yellow">generic entrywise extension of context-sensitive relations for terma</td>
452             <td class="snns top yellow">lexs ( ? ⦻*[?,?,?] ? )</td>
453             <td class="snnn top yellow">lexs_length lexs_lexs</td>
454             <td class="snnn top yellow">
455               <br />
456             </td>
457             <td class="ssnn top yellow">
458               <br />
459             </td>
460           </tr>
461           <tr>
462             <td class="snns top capitalize italic orange" />
463             <td class="snns top italic orange" />
464             <td class="snns top orange">
465               <br />
466             </td>
467             <td class="snnn top orange">
468               <br />
469             </td>
470             <td class="snnn top orange">
471               <br />
472             </td>
473             <td class="ssnn top orange">
474               <br />
475             </td>
476           </tr>
477           <tr>
478             <td class="snns top capitalize italic red">grammar</td>
479             <td class="snns top italic red">context-sensitive equivalences for terms</td>
480             <td class="snns top red">ceq</td>
481             <td class="snnn top red">ceq_ceq</td>
482             <td class="snnn top red">
483               <br />
484             </td>
485             <td class="ssnn top red">
486               <br />
487             </td>
488           </tr>
489           <tr>
490             <td class="nnns top capitalize italic red">
491               <br />
492             </td>
493             <td class="snns top italic red">same top term structure</td>
494             <td class="snns top red">tsts ( ? ≂ ? )</td>
495             <td class="snnn top red">tsts_tsts tsts_vector</td>
496             <td class="snnn top red">
497               <br />
498             </td>
499             <td class="ssnn top red">
500               <br />
501             </td>
502           </tr>
503           <tr>
504             <td class="nnns top capitalize italic red">
505               <br />
506             </td>
507             <td class="snns top italic red">closures</td>
508             <td class="snns top red">cl_weight ( ♯{?,?,?} )</td>
509             <td class="snnn top red">cl_restricted_weight ( ♯{?,?} )</td>
510             <td class="snnn top red">
511               <br />
512             </td>
513             <td class="ssnn top red">
514               <br />
515             </td>
516           </tr>
517           <tr>
518             <td class="nnns top capitalize italic red">
519               <br />
520             </td>
521             <td class="snns top italic red">internal syntax</td>
522             <td class="snns top red">genv</td>
523             <td class="snnn top red">
524               <br />
525             </td>
526             <td class="snnn top red">
527               <br />
528             </td>
529             <td class="ssnn top red">
530               <br />
531             </td>
532           </tr>
533           <tr>
534             <td class="nnns top capitalize italic red">
535               <br />
536             </td>
537             <td class="nnns top italic red">
538               <br />
539             </td>
540             <td class="snns top red">lenv</td>
541             <td class="snnn top red">lenv_weight ( ♯{?} )</td>
542             <td class="snnn top red">lenv_length ( |?| )</td>
543             <td class="ssnn top red">lenv_append ( ? @@ ? )</td>
544           </tr>
545           <tr>
546             <td class="nnns top capitalize italic red">
547               <br />
548             </td>
549             <td class="nnns top italic red">
550               <br />
551             </td>
552             <td class="snns top red">term</td>
553             <td class="snnn top red">term_weight ( ♯{?} )</td>
554             <td class="snnn top red">term_simple ( 𝐒⦃?⦄ )</td>
555             <td class="ssnn top red">term_vector ( Ⓐ?.? )</td>
556           </tr>
557           <tr>
558             <td class="nnns top capitalize italic red">
559               <br />
560             </td>
561             <td class="nnns top italic red">
562               <br />
563             </td>
564             <td class="snns top red">item</td>
565             <td class="snnn top red">
566               <br />
567             </td>
568             <td class="snnn top red">
569               <br />
570             </td>
571             <td class="ssnn top red">
572               <br />
573             </td>
574           </tr>
575           <tr>
576             <td class="nnss top capitalize italic red">
577               <br />
578             </td>
579             <td class="snss top italic red">external syntax</td>
580             <td class="snss top red">aarity</td>
581             <td class="snsn top red">
582               <br />
583             </td>
584             <td class="snsn top red">
585               <br />
586             </td>
587             <td class="sssn top red">
588               <br />
589             </td>
590           </tr>
591         </tbody>
592       </table>
593     </div>
594     <div class="spacer">
595       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
596     </div>
597     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
598       <br />
599     </div>
600     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
601       <a href="http://validator.w3.org/check?uri=referer">
602         <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
603       </a>
604       <a href="http://jigsaw.w3.org/css-validator/check/referer">
605         <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
606       </a>
607       <a href="http://www.w3.org/XML/">
608         <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
609       </a>
610       <a href="http://www.w3.org/Graphics/PNG/">
611         <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
612       </a>
613       <a href="http://www.anybrowser.org/campaign/">
614         <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
615       </a>
616     </div>
617     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
618       <br />
619     </div>
620     <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 27 Mar 2016 18:42:29 +0200</div>
621   </body>
622 </html>