How-_003ccode_003eavram_003c_002fcode_003e-Thinks.html 9.4 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159
  1. <html lang="en">
  2. <head>
  3. <title>How @code{avram} Thinks - avram - a virtual machine code interpreter</title>
  4. <meta http-equiv="Content-Type" content="text/html">
  5. <meta name="description" content="avram - a virtual machine code interpreter">
  6. <meta name="generator" content="makeinfo 4.13">
  7. <link title="Top" rel="start" href="index.html#Top">
  8. <link rel="up" href="Virtual-Code-Semantics.html#Virtual-Code-Semantics" title="Virtual Code Semantics">
  9. <link rel="prev" href="A-Simple-Lisp-Like-Language.html#A-Simple-Lisp-Like-Language" title="A Simple Lisp Like Language">
  10. <link rel="next" href="Variable-Freedom.html#Variable-Freedom" title="Variable Freedom">
  11. <link href="http://www.gnu.org/software/texinfo/" rel="generator-home" title="Texinfo Homepage">
  12. <meta http-equiv="Content-Style-Type" content="text/css">
  13. <style type="text/css"><!--
  14. pre.display { font-family:inherit }
  15. pre.format { font-family:inherit }
  16. pre.smalldisplay { font-family:inherit; font-size:smaller }
  17. pre.smallformat { font-family:inherit; font-size:smaller }
  18. pre.smallexample { font-size:smaller }
  19. pre.smalllisp { font-size:smaller }
  20. span.sc { font-variant:small-caps }
  21. span.roman { font-family:serif; font-weight:normal; }
  22. span.sansserif { font-family:sans-serif; font-weight:normal; }
  23. --></style>
  24. </head>
  25. <body>
  26. <div class="node">
  27. <a name="How-%3ccode%3eavram%3c%2fcode%3e-Thinks"></a>
  28. <a name="How-_003ccode_003eavram_003c_002fcode_003e-Thinks"></a>
  29. <p>
  30. Next:&nbsp;<a rel="next" accesskey="n" href="Variable-Freedom.html#Variable-Freedom">Variable Freedom</a>,
  31. Previous:&nbsp;<a rel="previous" accesskey="p" href="A-Simple-Lisp-Like-Language.html#A-Simple-Lisp-Like-Language">A Simple Lisp Like Language</a>,
  32. Up:&nbsp;<a rel="up" accesskey="u" href="Virtual-Code-Semantics.html#Virtual-Code-Semantics">Virtual Code Semantics</a>
  33. <hr>
  34. </div>
  35. <h4 class="subsection">2.7.5 How <code>avram</code> Thinks</h4>
  36. <p>The definitions in the standard <code>silly</code> library pertaining to the
  37. basic properties of the operator can provide a good intuitive
  38. illustration of how computations are performed by <code>avram</code>. This
  39. task is approached in the guise of a few trivial correctness proofs
  40. about them. Conveniently, as an infeasibly small language, <code>silly</code>
  41. is an ideal candidate for analysis by formal methods.
  42. <p>Technically the semantic function [[<small class="dots">...</small>]] has not been defined on
  43. identifiers, but we can easily extend it to them by stipulating that the
  44. meaning of an identifier <var>x</var> is the meaning of the program
  45. <a name="index-identifiers-271"></a><var>main</var><code> = </code><var>x</var> when linked with a library containing the
  46. declaration of <var>x</var>, where <var>main</var> is an identifier
  47. not appearing elsewhere in the library.
  48. <p>With this idea in mind, the following &ldquo;theorems&rdquo; can be stated,
  49. all of which have a similar proof. The variables <var>x</var> and <var>y</var>
  50. stand for any tree, and the variable <var>f</var> stands for any tree other
  51. than <code>nil</code>.
  52. <dl>
  53. <dt><em>T0</em><dd>[[<code>identity</code>]] <var>x</var> = <var>x</var>
  54. <br><dt><em>T1</em><dd>[[<code>left</code>]] <code>(</code><var>x</var><code>,</code><var>y</var><code>)</code> = <var>x</var>
  55. <br><dt><em>T2</em><dd>[[<code>right</code>]] <code>(</code><var>x</var><code>,</code><var>y</var><code>)</code> = <var>y</var>
  56. <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>
  57. <br><dt><em>T5</em><dd>[[<code>constant_nil</code>]] <var>x</var> = <code>nil</code>
  58. </dl>
  59. <p class="noindent">Replacing each identifier with its defining expression directly
  60. demonstrates a logical equivalence between the relevant theorem and one
  61. 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>.
  62. <p>For more of a challenge, it is possible to prove the next theorem.
  63. <dl>
  64. <dt><em>T6</em><dd>For non-<code>nil</code> <var>f</var> and <var>g</var>,
  65. ([[<code>couple</code>]] <code>(</code><var>f</var><code>,</code><var>g</var><code>)</code>) <var>x</var> =
  66. <code>(</code><var>f</var> <var>x</var><code>,</code><var>g</var> <var>x</var><code>)</code>
  67. </dl>
  68. <p class="noindent">The proof is a routine calculation. Beware of the distinction between
  69. the mathematical <code>nil</code> and the <code>silly</code> identifier <code>nil</code>.
  70. <pre class="format">
  71. ([[<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>
  72. by substitution of <code>couple</code> with its definition in the standard library
  73. = (<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>
  74. by definition of the semantic function [[<small class="dots">...</small>]] regarding pairs
  75. = (<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>
  76. by substitution of <code>nil</code> from its definition in the standard library
  77. = (<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>
  78. by definition of the semantic function in the case of [[<code>()</code>]]
  79. = (<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>
  80. by property <em>P6</em> (twice)
  81. = <code>((</code><var>f</var><code>,nil),</code><var>g</var><code>) </code><var>x</var>
  82. by theorems <em>T1</em>, <em>T2</em>, and <em>T5</em>
  83. = <code>(</code><var>f</var> <var>x</var><code>,</code><var>g</var> <var>x</var><code>)</code>
  84. by property <em>P6</em> again.
  85. </pre>
  86. <p>Something to observe about this proof is that it might just as well have
  87. been done automatically. Every step is either the substitution of an
  88. identifier or a pattern match against existing theorems and properties
  89. of the operator. Another thing to note is that the use of identifiers
  90. and previously established theorems helps to make the proof human
  91. readable, but is not a logical necessity. An equivalent proof could have
  92. been expressed entirely in terms of the properties of the operator. If
  93. one envisions a proof like this being performed blindly and
  94. mechanically, without the running commentary or other amenities, that
  95. would not be a bad way of thinking about what takes place when
  96. <code>avram</code> executes virtual code.
  97. <p>Three more theorems have similar proofs. For non-<code>nil</code>
  98. trees <var>p</var>, <var>f</var> and <var>g</var>, and any trees
  99. <var>x</var> and <var>k</var>:
  100. <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>
  101. <dl>
  102. <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>
  103. <br><dt><em>T8</em><dd>([[<code>constant</code>]] <var>k</var>) <var>x</var> = <var>k</var>
  104. <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> =
  105. <var>f</var> <var>x</var> if
  106. <var>p</var> <var>x</var> is non-<code>nil</code>,
  107. but <var>g</var> <var>x</var> if <var>p</var> <var>x</var> = <code>nil</code>
  108. </dl>
  109. <p class="noindent">The proofs of these theorems are routine calculations analogous to the
  110. proof of <em>T6</em>. Here is a proof of theorem <em>T7</em> for good
  111. measure.
  112. <pre class="format">
  113. ([[<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>
  114. </pre>
  115. <p>by substitution of <code>compose</code> with its definition in the standard library
  116. <pre class="format">
  117. = (<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>
  118. by definition of the semantic function
  119. = <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>
  120. by theorem <em>T6</em>
  121. = <code>((</code><var>f</var><code>,</code><var>g</var><code>),nil) </code><var>x</var>
  122. by theorems <em>T0</em> and <em>T5</em>
  123. = <var>f</var> <var>g</var> <var>x</var>
  124. by property <em>P5</em> of the operator.
  125. </pre>
  126. </body></html>