txlyre
/
avram


			
				
					
						
						
							123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117
							<html lang="en">
<head>
<title>Operator Generalization - 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="Exception-Handling.html#Exception-Handling" title="Exception Handling">
<link rel="prev" href="A-Hierarchy-of-Sets.html#A-Hierarchy-of-Sets" title="A Hierarchy of Sets">
<link rel="next" href="Error-Messages.html#Error-Messages" title="Error Messages">
<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="Operator-Generalization"></a>
<p>
Next:&nbsp;<a rel="next" accesskey="n" href="Error-Messages.html#Error-Messages">Error Messages</a>,
Previous:&nbsp;<a rel="previous" accesskey="p" href="A-Hierarchy-of-Sets.html#A-Hierarchy-of-Sets">A Hierarchy of Sets</a>,
Up:&nbsp;<a rel="up" accesskey="u" href="Exception-Handling.html#Exception-Handling">Exception Handling</a>
<hr>
</div>

<h5 class="subsubsection">2.7.15.2 Operator Generalization</h5>

<p>Each set in the hierarchy induces a structure preserving <code>cons</code>
<a name="index-g_t_0040code_007bcons_007d-351"></a>operator, denoted <code>cons_</code><var>n</var> for the <var>n</var>th level
set, and satisfying this equation.

     <dl>
<dt><em>E10</em><dd><code>cons_</code><var>n</var><code>(</code><var>x</var><code>_</code><var>n</var><code>,</code><var>y</var><code>_</code><var>n</var><code>)</code> =
<code>(cons(</code><var>x</var><code>,</code><var>y</var><code>))_</code><var>n</var>
</dl>

<p class="noindent">It will be convenient to generalize all of these <code>cons</code> operators to be
defined on members of other sets than their own.

     <dl>
<dt><em>E11</em><dd>For <var>m</var> greater than <var>n</var>,
&nbsp;<!-- /@w --> &nbsp;<!-- /@w --> &nbsp;<!-- /@w --> <code>cons_</code><var>n</var><code>(</code><var>x</var><code>_</code><var>m</var><code>,</code><var>y</var><code>_</code><var>p</var><code>)</code> =
<var>x</var><code>_</code><var>m</var>
</dl>

<p class="noindent">In this equation, <var>p</var> is unrestricted. The intuition is that
if the left operand of a <code>cons</code> is the result of a computation that
went wrong due to an exceptional condition (more exceptional than
<var>n</var>, the level already in effect), then the exceptional
result becomes the whole result.

   <p>It is tempting to hazard a slightly stronger statement, which is that
this equation holds even if <var>y</var><code>_</code><var>p</var> is equal to some
expression <var>f</var> <var>x</var> that is undefined according to the
operator semantics. This stipulation would correspond to an
implementation in which the right operand isn't evaluated after an error
is detected in the left, but there are two problems with it.

     <ul>
<li>This semantics might unreasonably complicate a concurrent
implementation of the virtual machine. If evaluation leads to
non-termination in some cases where the result is undefined (as it certainly
would in any possible implementation consistent with cases where it's
defined), then the mechanism that evaluates the right side of a pair
must be interruptible in case an exception is detected in the left. 
<li>It is beyond the expressive power of the present mathematical
framework to make such a statement, because it entails universal
quantification over non-members of the constructed sets, which includes
<a name="index-universal-quantification-352"></a>almost everything. 
</ul>

<p class="noindent">Nevertheless, the implementation in <code>avram</code> is sequential and does
indeed behave as proposed, with no practical difficulty. As for any
deficiency in the theory, it could be banished by recasting the
semantics in terms of a calculus of expressions with formal rules of
manipulation. An operand to the <code>cons</code> operator would be identified
not with a member of a semantic domain, but with the expression used to
write it down, and then even &ldquo;undefinedness&rdquo; could be
<a name="index-undefined-expressions-353"></a>defined. However, the present author's preference in computing as in
<a name="index-author-354"></a>life is to let some things remain a mystery rather than to abandon the
quest for meaning entirely.

   <p>A comparable condition applies in cases where the right side of a pair
represents an exceptional result.

     <dl>
<dt><em>E12</em><dd>For <var>m</var> greater than <var>n</var>,
&nbsp;<!-- /@w --> &nbsp;<!-- /@w --> <code>cons_</code><var>n</var><code>(</code><var>x</var><code>_</code><var>n</var><code>,</code><var>y</var><code>_</code><var>m</var><code>)</code> =
<var>y</var><code>_</code><var>m</var>
</dl>

   <p>Whereas an infinitude of <code>cons</code> operators has been needed, it will
<a name="index-g_t_0040code_007bcons_007d-355"></a>be possible to get by with only one invisible operator, as before, by
generalizing it in the following way to operands on any level of the
hierarchy.

     <dl>
<dt><em>P43</em><dd><var>f</var><code>_</code><var>n</var> <var>x</var><code>_</code><var>n</var> = <code>(</code><var>f</var> <var>x</var><code>)_</code><var>n</var>
<br><dt><em>P44</em><dd>For distinct <var>n</var> and <var>m</var>, &nbsp;<!-- /@w --><var>f</var><code>_</code><var>n</var> <var>x</var><code>_</code><var>m</var> = <var>x</var><code>_</code><var>m</var>
</dl>

<p class="noindent">That is, the result of evaluating two operands on the same level is the
image relative to that level of the result of their respective images on
the bottom level, but the result of evaluating two operands on different
levels is the same as the right operand.

   </body></html>