txlyre
/
avram


			
				
					
						
						
							12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576
							<html lang="en">
<head>
<title>On Equality - 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-New-Operator.html#A-New-Operator" title="A New Operator">
<link rel="next" href="A-Minimal-Set-of-Properties.html#A-Minimal-Set-of-Properties" title="A Minimal Set of Properties">
<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="On-Equality"></a>
<p>
Next:&nbsp;<a rel="next" accesskey="n" href="A-Minimal-Set-of-Properties.html#A-Minimal-Set-of-Properties">A Minimal Set of Properties</a>,
Previous:&nbsp;<a rel="previous" accesskey="p" href="A-New-Operator.html#A-New-Operator">A New Operator</a>,
Up:&nbsp;<a rel="up" accesskey="u" href="Virtual-Code-Semantics.html#Virtual-Code-Semantics">Virtual Code Semantics</a>
<hr>
</div>

<h4 class="subsection">2.7.2 On Equality</h4>

<p><a name="index-equality-241"></a>One example of a property this operator should have, for reasons that
will not be immediately clear, is that for any trees <var>x</var> and
<var>k</var>, the equality <code>cons(cons(nil,</code><var>k</var><code>),nil) </code><var>x</var><code> =
</code><var>k</var> always holds. 
Even though the present exposition opts for readability over formality,
statements like these demand clarification of the notion of
equality. Some of the more pedantic points in <a href="Raw-Material.html#Raw-Material">Raw Material</a> may be needed
for the following ideas to hold water.

     <ul>
<li>As originally stipulated, it is always possible to distinguish
<code>nil</code> from any member of the set. We can therefore decide on this
basis whether <var>a</var><code> = </code><var>b</var> whenever at least one of them is <code>nil</code>. 
<li>Where neither <var>a</var> nor <var>b</var> is <code>nil</code> in an expression
<var>a</var><code> = </code><var>b</var>, but rather something of the form
<code>cons(</code><var>x</var><code>,</code><var>y</var><code>)</code>, the equality holds if and only
if both pairs of corresponding subexpressions are equal. If at least one
member of each pair of corresponding subexpressions is <code>nil</code>, the
question is settled, but otherwise there is recourse to their respective
subexpressions, and so on. This condition follows from the uniqueness property
of the <code>cons</code> operator. 
<li>If one side of an equality is of the form
<var>x</var> <var>y</var>, or is defined in terms of such an expression,
but <code>(</code><var>x</var><code>,</code><var>y</var><code>)</code> is one of those pairs with which the operator
associates no result, then the equality holds if and only if the other
side is similarly ill defined. 
<li>Statements involving universal quantification (i.e.,
<a name="index-universal-quantification-242"></a><a name="index-undefined-expressions-243"></a>beginning with words similar to &ldquo;for any tree <var>x</var> <small class="dots">...</small>&rdquo;)
obviously do not apply to instances of a variable (<var>x</var>) outside
the indicated set (trees). Hence, they are not refuted by any
consequence of identifying a variable with an undefined expression. 
</ul>

   <p>Readers who are aware of such issues as pointer equality or intensional
<a name="index-pointer-equality-244"></a><a name="index-pointers-245"></a>versus extensional equality of functions are urged to forget all about
them in the context of this document, and abide only by what is
stated. Other readers should ignore this paragraph.

   </body></html>