123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159 |
- <html lang="en">
- <head>
- <title>How @code{avram} Thinks - avram - a virtual machine code interpreter</title>
- <meta http-equiv="Content-Type" content="text/html">
- <meta name="description" content="avram - a virtual machine code interpreter">
- <meta name="generator" content="makeinfo 4.13">
- <link title="Top" rel="start" href="index.html#Top">
- <link rel="up" href="Virtual-Code-Semantics.html#Virtual-Code-Semantics" title="Virtual Code Semantics">
- <link rel="prev" href="A-Simple-Lisp-Like-Language.html#A-Simple-Lisp-Like-Language" title="A Simple Lisp Like Language">
- <link rel="next" href="Variable-Freedom.html#Variable-Freedom" title="Variable Freedom">
- <link href="http://www.gnu.org/software/texinfo/" rel="generator-home" title="Texinfo Homepage">
- <meta http-equiv="Content-Style-Type" content="text/css">
- <style type="text/css"><!--
- pre.display { font-family:inherit }
- pre.format { font-family:inherit }
- pre.smalldisplay { font-family:inherit; font-size:smaller }
- pre.smallformat { font-family:inherit; font-size:smaller }
- pre.smallexample { font-size:smaller }
- pre.smalllisp { font-size:smaller }
- span.sc { font-variant:small-caps }
- span.roman { font-family:serif; font-weight:normal; }
- span.sansserif { font-family:sans-serif; font-weight:normal; }
- --></style>
- </head>
- <body>
- <div class="node">
- <a name="How-%3ccode%3eavram%3c%2fcode%3e-Thinks"></a>
- <a name="How-_003ccode_003eavram_003c_002fcode_003e-Thinks"></a>
- <p>
- Next: <a rel="next" accesskey="n" href="Variable-Freedom.html#Variable-Freedom">Variable Freedom</a>,
- Previous: <a rel="previous" accesskey="p" href="A-Simple-Lisp-Like-Language.html#A-Simple-Lisp-Like-Language">A Simple Lisp Like Language</a>,
- Up: <a rel="up" accesskey="u" href="Virtual-Code-Semantics.html#Virtual-Code-Semantics">Virtual Code Semantics</a>
- <hr>
- </div>
- <h4 class="subsection">2.7.5 How <code>avram</code> Thinks</h4>
- <p>The definitions in the standard <code>silly</code> library pertaining to the
- basic properties of the operator can provide a good intuitive
- illustration of how computations are performed by <code>avram</code>. This
- task is approached in the guise of a few trivial correctness proofs
- about them. Conveniently, as an infeasibly small language, <code>silly</code>
- is an ideal candidate for analysis by formal methods.
- <p>Technically the semantic function [[<small class="dots">...</small>]] has not been defined on
- identifiers, but we can easily extend it to them by stipulating that the
- meaning of an identifier <var>x</var> is the meaning of the program
- <a name="index-identifiers-271"></a><var>main</var><code> = </code><var>x</var> when linked with a library containing the
- declaration of <var>x</var>, where <var>main</var> is an identifier
- not appearing elsewhere in the library.
- <p>With this idea in mind, the following “theorems” can be stated,
- all of which have a similar proof. The variables <var>x</var> and <var>y</var>
- stand for any tree, and the variable <var>f</var> stands for any tree other
- than <code>nil</code>.
- <dl>
- <dt><em>T0</em><dd>[[<code>identity</code>]] <var>x</var> = <var>x</var>
- <br><dt><em>T1</em><dd>[[<code>left</code>]] <code>(</code><var>x</var><code>,</code><var>y</var><code>)</code> = <var>x</var>
- <br><dt><em>T2</em><dd>[[<code>right</code>]] <code>(</code><var>x</var><code>,</code><var>y</var><code>)</code> = <var>y</var>
- <br><dt><em>T4</em><dd>[[<code>meta</code>]] <code>(</code><var>f</var><code>,</code><var>x</var><code>)</code> = <var>f</var><code> (</code><var>f</var><code>,</code><var>x</var><code>)</code>
- <br><dt><em>T5</em><dd>[[<code>constant_nil</code>]] <var>x</var> = <code>nil</code>
- </dl>
- <p class="noindent">Replacing each identifier with its defining expression directly
- demonstrates a logical equivalence between the relevant theorem and one
- of the basic operator properties postulated in <a href="A-Minimal-Set-of-Properties.html#A-Minimal-Set-of-Properties">A Minimal Set of Properties</a>.
- <p>For more of a challenge, it is possible to prove the next theorem.
- <dl>
- <dt><em>T6</em><dd>For non-<code>nil</code> <var>f</var> and <var>g</var>,
- ([[<code>couple</code>]] <code>(</code><var>f</var><code>,</code><var>g</var><code>)</code>) <var>x</var> =
- <code>(</code><var>f</var> <var>x</var><code>,</code><var>g</var> <var>x</var><code>)</code>
- </dl>
- <p class="noindent">The proof is a routine calculation. Beware of the distinction between
- the mathematical <code>nil</code> and the <code>silly</code> identifier <code>nil</code>.
- <pre class="format">
- ([[<code>couple</code>]] <code>(</code><var>f</var><code>,</code><var>g</var><code>)</code>) <var>x</var> = ([[<code>((((left,nil),constant_nil),nil),right)</code>]] <code>(</code><var>f</var><code>,</code><var>g</var><code>)</code>) <var>x</var>
- by substitution of <code>couple</code> with its definition in the standard library
- = (<code>((((</code>[[<code>left</code>]]<code>,</code>[[<code>nil</code>]]<code>),</code>[[<code>constant_nil</code>]]<code>),</code>[[<code>nil</code>]])<code>,</code>[[<code>right</code>]]<code>)</code> <code>(</code><var>f</var><code>,</code><var>g</var><code>)</code>) <var>x</var>
- by definition of the semantic function [[<small class="dots">...</small>]] regarding pairs
- = (<code>((((</code>[[<code>left</code>]]<code>,</code>[[<code>()</code>]]<code>),</code>[[<code>constant_nil</code>]]<code>),</code>[[<code>()</code>]])<code>,</code>[[<code>right</code>]]<code>)</code> <code>(</code><var>f</var><code>,</code><var>g</var><code>)</code>) <var>x</var>
- by substitution of <code>nil</code> from its definition in the standard library
- = (<code>((((</code>[[<code>left</code>]]<code>,</code><code>nil</code><code>),</code>[[<code>constant_nil</code>]]<code>),</code><code>nil</code>)<code>,</code>[[<code>right</code>]]<code>)</code> <code>(</code><var>f</var><code>,</code><var>g</var><code>)</code>) <var>x</var>
- by definition of the semantic function in the case of [[<code>()</code>]]
- = (<code>(</code>[[<code>left</code>]] <code>(</code><var>f</var><code>,</code><var>g</var><code>),</code>[[<code>constant_nil</code>]] <code>(</code><var>f</var><code>,</code><var>g</var><code>)),</code>[[<code>right</code>]] <code>(</code><var>f</var><code>,</code><var>g</var><code>)</code>) <var>x</var>
- by property <em>P6</em> (twice)
- = <code>((</code><var>f</var><code>,nil),</code><var>g</var><code>) </code><var>x</var>
- by theorems <em>T1</em>, <em>T2</em>, and <em>T5</em>
- = <code>(</code><var>f</var> <var>x</var><code>,</code><var>g</var> <var>x</var><code>)</code>
- by property <em>P6</em> again.
- </pre>
- <p>Something to observe about this proof is that it might just as well have
- been done automatically. Every step is either the substitution of an
- identifier or a pattern match against existing theorems and properties
- of the operator. Another thing to note is that the use of identifiers
- and previously established theorems helps to make the proof human
- readable, but is not a logical necessity. An equivalent proof could have
- been expressed entirely in terms of the properties of the operator. If
- one envisions a proof like this being performed blindly and
- mechanically, without the running commentary or other amenities, that
- would not be a bad way of thinking about what takes place when
- <code>avram</code> executes virtual code.
- <p>Three more theorems have similar proofs. For non-<code>nil</code>
- trees <var>p</var>, <var>f</var> and <var>g</var>, and any trees
- <var>x</var> and <var>k</var>:
- <a name="index-g_t_0040code_007bcompose_007d-272"></a><a name="index-g_t_0040code_007bconstant_007d-273"></a><a name="index-g_t_0040code_007bconditional_007d-274"></a>
- <dl>
- <dt><em>T7</em><dd>([[<code>compose</code>]] <code>(</code><var>f</var><code>,</code><var>g</var><code>)</code>) <var>x</var> = <var>f</var> <var>g</var> <var>x</var>
- <br><dt><em>T8</em><dd>([[<code>constant</code>]] <var>k</var>) <var>x</var> = <var>k</var>
- <br><dt><em>T9</em><dd>([[<code>conditional</code>]] <code>(</code><var>p</var><code>,(</code><var>f</var><code>,</code><var>g</var><code>)</code>) <var>x</var> =
- <var>f</var> <var>x</var> if
- <var>p</var> <var>x</var> is non-<code>nil</code>,
- but <var>g</var> <var>x</var> if <var>p</var> <var>x</var> = <code>nil</code>
- </dl>
- <p class="noindent">The proofs of these theorems are routine calculations analogous to the
- proof of <em>T6</em>. Here is a proof of theorem <em>T7</em> for good
- measure.
- <pre class="format">
- ([[<code>compose</code>]] <code>(</code><var>f</var><code>,</code><var>g</var><code>)</code>) <var>x</var> = ([[<code>couple(identity,constant_nil)</code>]] <code>(</code><var>f</var><code>,</code><var>g</var><code>)</code>) <var>x</var>
- </pre>
- <p>by substitution of <code>compose</code> with its definition in the standard library
- <pre class="format">
- = (<code>(</code>[[<code>couple</code>]] <code>(</code>[[<code>identity</code>]]<code>,</code>[[<code>constant_nil</code>]]<code>))(</code><var>f</var><code>,</code><var>g</var><code>)</code>) <var>x</var>
- by definition of the semantic function
- = <code>(</code>[[<code>identity</code>]] <code>(</code><var>f</var><code>,</code><var>g</var><code>),</code>[[<code>constant_nil</code>]]<code> (</code><var>f</var><code>,</code><var>g</var><code>)) </code><var>x</var>
- by theorem <em>T6</em>
- = <code>((</code><var>f</var><code>,</code><var>g</var><code>),nil) </code><var>x</var>
- by theorems <em>T0</em> and <em>T5</em>
- = <var>f</var> <var>g</var> <var>x</var>
- by property <em>P5</em> of the operator.
- </pre>
- </body></html>
|