On-Equality.html 7.4 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133
  1. <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html401/loose.dtd">
  2. <html>
  3. <!-- Created on November 8, 2012 by texi2html 1.82
  4. texi2html was written by:
  5. Lionel Cons <[email protected]> (original author)
  6. Karl Berry <[email protected]>
  7. Olaf Bachmann <[email protected]>
  8. and many others.
  9. Maintained by: Many creative people.
  10. Send bugs and suggestions to <[email protected]>
  11. -->
  12. <head>
  13. <title>avram - a virtual machine code interpreter: 2.7.2 On Equality</title>
  14. <meta name="description" content="avram - a virtual machine code interpreter: 2.7.2 On Equality">
  15. <meta name="keywords" content="avram - a virtual machine code interpreter: 2.7.2 On Equality">
  16. <meta name="resource-type" content="document">
  17. <meta name="distribution" content="global">
  18. <meta name="Generator" content="texi2html 1.82">
  19. <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  20. <style type="text/css">
  21. <!--
  22. a.summary-letter {text-decoration: none}
  23. blockquote.smallquotation {font-size: smaller}
  24. pre.display {font-family: serif}
  25. pre.format {font-family: serif}
  26. pre.menu-comment {font-family: serif}
  27. pre.menu-preformatted {font-family: serif}
  28. pre.smalldisplay {font-family: serif; font-size: smaller}
  29. pre.smallexample {font-size: smaller}
  30. pre.smallformat {font-family: serif; font-size: smaller}
  31. pre.smalllisp {font-size: smaller}
  32. span.roman {font-family:serif; font-weight:normal;}
  33. span.sansserif {font-family:sans-serif; font-weight:normal;}
  34. ul.toc {list-style: none}
  35. -->
  36. </style>
  37. </head>
  38. <body lang="en" bgcolor="#FFFFFF" text="#000000" link="#0000FF" vlink="#800080" alink="#FF0000">
  39. <a name="On-Equality"></a>
  40. <table cellpadding="1" cellspacing="1" border="0">
  41. <tr><td valign="middle" align="left">[<a href="A-New-Operator.html#A-New-Operator" title="Previous section in reading order"> &lt; </a>]</td>
  42. <td valign="middle" align="left">[<a href="A-Minimal-Set-of-Properties.html#A-Minimal-Set-of-Properties" title="Next section in reading order"> &gt; </a>]</td>
  43. <td valign="middle" align="left"> &nbsp; </td>
  44. <td valign="middle" align="left">[<a href="Virtual-Machine-Specification.html#Virtual-Machine-Specification" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
  45. <td valign="middle" align="left">[<a href="Virtual-Code-Semantics.html#Virtual-Code-Semantics" title="Up section"> Up </a>]</td>
  46. <td valign="middle" align="left">[<a href="Library-Reference.html#Library-Reference" title="Next chapter"> &gt;&gt; </a>]</td>
  47. <td valign="middle" align="left"> &nbsp; </td>
  48. <td valign="middle" align="left"> &nbsp; </td>
  49. <td valign="middle" align="left"> &nbsp; </td>
  50. <td valign="middle" align="left"> &nbsp; </td>
  51. <td valign="middle" align="left">[<a href="avram.html#Top" title="Cover (top) of document">Top</a>]</td>
  52. <td valign="middle" align="left">[<a href="avram_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
  53. <td valign="middle" align="left">[<a href="Function-Index.html#Function-Index" title="Index">Index</a>]</td>
  54. <td valign="middle" align="left">[<a href="avram_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
  55. </tr></table>
  56. <hr size="1">
  57. <a name="On-Equality-1"></a>
  58. <h3 class="subsection">2.7.2 On Equality</h3>
  59. <a name="index-equality"></a>
  60. <p>One example of a property this operator should have, for reasons that
  61. will not be immediately clear, is that for any trees <code><var>x</var></code> and
  62. <code><var>k</var></code>, the equality <code>cons(cons(nil,<code><var>k</var>),nil) <var>x</var></code> =
  63. <code><var>k</var></code></code> always holds.
  64. Even though the present exposition opts for readability over formality,
  65. statements like these demand clarification of the notion of
  66. equality. Some of the more pedantic points in <a href="Raw-Material.html#Raw-Material">Raw Material</a> may be needed
  67. for the following ideas to hold water.
  68. </p>
  69. <ul>
  70. <li> As originally stipulated, it is always possible to distinguish
  71. <code>nil</code> from any member of the set. We can therefore decide on this
  72. basis whether <code><var>a</var> = <var>b</var></code> whenever at least one of them is <code>nil</code>.
  73. </li><li> Where neither <code><var>a</var></code> nor <code><var>b</var></code> is <code>nil</code> in an expression
  74. <code><var>a</var> = <var>b</var></code>, but rather something of the form
  75. <code>cons(<var>x</var>,<var>y</var>)</code>, the equality holds if and only
  76. if both pairs of corresponding subexpressions are equal. If at least one
  77. member of each pair of corresponding subexpressions is <code>nil</code>, the
  78. question is settled, but otherwise there is recourse to their respective
  79. subexpressions, and so on. This condition follows from the uniqueness property
  80. of the <code>cons</code> operator.
  81. </li><li> If one side of an equality is of the form
  82. <code><var>x</var> <var>y</var></code>, or is defined in terms of such an expression,
  83. but <code>(<var>x</var>,<var>y</var>)</code> is one of those pairs with which the operator
  84. associates no result, then the equality holds if and only if the other
  85. side is similarly ill defined.
  86. </li><li> Statements involving universal quantification (i.e.,
  87. <a name="index-universal-quantification"></a>
  88. <a name="index-undefined-expressions"></a>
  89. beginning with words similar to &ldquo;for any tree <code><var>x</var></code> &hellip;&rdquo;)
  90. obviously do not apply to instances of a variable (<code><var>x</var></code>) outside
  91. the indicated set (trees). Hence, they are not refuted by any
  92. consequence of identifying a variable with an undefined expression.
  93. </li></ul>
  94. <p>Readers who are aware of such issues as pointer equality or intensional
  95. <a name="index-pointer-equality"></a>
  96. <a name="index-pointers-1"></a>
  97. versus extensional equality of functions are urged to forget all about
  98. them in the context of this document, and abide only by what is
  99. stated. Other readers should ignore this paragraph.
  100. </p>
  101. <hr size="1">
  102. <table cellpadding="1" cellspacing="1" border="0">
  103. <tr><td valign="middle" align="left">[<a href="A-New-Operator.html#A-New-Operator" title="Previous section in reading order"> &lt; </a>]</td>
  104. <td valign="middle" align="left">[<a href="A-Minimal-Set-of-Properties.html#A-Minimal-Set-of-Properties" title="Next section in reading order"> &gt; </a>]</td>
  105. <td valign="middle" align="left"> &nbsp; </td>
  106. <td valign="middle" align="left">[<a href="Virtual-Machine-Specification.html#Virtual-Machine-Specification" title="Beginning of this chapter or previous chapter"> &lt;&lt; </a>]</td>
  107. <td valign="middle" align="left">[<a href="Virtual-Code-Semantics.html#Virtual-Code-Semantics" title="Up section"> Up </a>]</td>
  108. <td valign="middle" align="left">[<a href="Library-Reference.html#Library-Reference" title="Next chapter"> &gt;&gt; </a>]</td>
  109. <td valign="middle" align="left"> &nbsp; </td>
  110. <td valign="middle" align="left"> &nbsp; </td>
  111. <td valign="middle" align="left"> &nbsp; </td>
  112. <td valign="middle" align="left"> &nbsp; </td>
  113. <td valign="middle" align="left">[<a href="avram.html#Top" title="Cover (top) of document">Top</a>]</td>
  114. <td valign="middle" align="left">[<a href="avram_toc.html#SEC_Contents" title="Table of contents">Contents</a>]</td>
  115. <td valign="middle" align="left">[<a href="Function-Index.html#Function-Index" title="Index">Index</a>]</td>
  116. <td valign="middle" align="left">[<a href="avram_abt.html#SEC_About" title="About (help)"> ? </a>]</td>
  117. </tr></table>
  118. <p>
  119. <font size="-1">
  120. This document was generated on <i>November 8, 2012</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  121. </font>
  122. <br>
  123. </p>
  124. </body>
  125. </html>