Skip to content

Commit

Permalink
The reduction process needs revamping... church numerals are breaking…
Browse files Browse the repository at this point in the history 
… on it. However it appears SUCC works, and I think PLUS will too, but well ... reduction
  • Loading branch information
@hellertime
hellertime committed Aug 17, 2007
1 parent ba02d4e commit 803c74a
Show file tree
Hide file tree
Showing 2 changed files with 234 additions and 3 deletions.
36 changes: 33 additions & 3 deletions js/lambda.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -250,7 +250,7 @@ function ()

if(this.var_p(expression))
{
console.log("No variable occurs bound in an expression consisting of a single variable or constant.");
// console.log("No variable occurs bound in an expression consisting of a single variable or constant.");
return false;
}

Expand Down Expand Up @@ -309,7 +309,8 @@ function ()
var redex = null;
if(this.application_p(node))
{
var head = this.application_head(node);
var head = this.application_head(node),
tail = this.application_tail(node);
if(this.abstraction_p(head))
{
redex = node;
Expand All @@ -322,13 +323,18 @@ function ()
this.substitute_term_in_expression(head,node,expansion);
redex = node;
}

if(this.application_p(tail) || this.abstraction_p(tail))
{
redex = this.find_next_redex(tail,environment);
}
}
else
{
redex = this.find_next_redex(head,environment);
if(!redex)
{
redex = this.find_next_redex(this.application_tail(node),environment);
redex = this.find_next_redex(tail,environment);
}
}
}
Expand All @@ -348,6 +354,30 @@ function ()
var abstraction = this.application_head(redex),
subst_term = this.application_tail(redex);

var expanded_var = null;
if(this.var_p(abstraction))
{
expanded_var = this.expand_var(abstraction,env);
if(this.var_p(expanded_var))
{
if(expanded_var === abstraction)
{
return null;
}

while(this.var_p(expanded_var))
{
abstraction = expanded_var;
expanded_var = this.expand_var(expanded_var,env);
if(abstraction === expanded_var)
{
return null;
}
}
}
abstraction = expanded_var;
}

while(this.occurs_bound(abstraction,subst_term))
{
if(!this.prime_rewrite_var(subst_term))
Expand Down
201 changes: 201 additions & 0 deletions prelude.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -185,11 +185,212 @@
</dl>
</div>

<h4>Church Numerals</h4>

<pre>
SUCC allows us to define any number once we have 0.
</pre>

<strong>SUCC</strong>
<div id="SUCC" class="lambda-exp">
<dl>
<dt><var>n</var>
<dd>
<dl>
<dt><var>f</var></dt>
<dd>
<dl>
<dt><var>x</var></dt>
<dd>
<ol>
<li><var>f</var></li>
<li>
<ol>
<li>
<ol>
<li><var>n</var></li>
<li><var>f</var></li>
</ol>
</li>
<li><var>x</var></li>
</ol>
</li>
</ol>
</dd>
</dl>
</dd>
</dl>
</dd>
</dl>
</div>

<pre>
Most examples only define ZERO - THREE in church numerals,
and since each numeral is just SUCC applied to the previous
one there is really no need to define more (really ZERO and
SUCC should be all we need)

But since its slow to have to compute ONE each time we need it,
a few are defined here just for example.
</pre>

<strong>ZERO</strong>
<em>It's &lt;FALSE&gt;, Surprise!</em>
<div id="ZERO" class="lambda-exp">
<var>FALSE</var>
</div>

<strong>ONE</strong>
<div id="ONE" class="lambda-exp">
<dl>
<dt><var>f</var></dt>
<dd>
<dl>
<dt><var>x</var></dt>
<dd>
<ol>
<li><var>f</var></li>
<li><var>x</var></li>
</ol>
</dd>
</dl>
</dd>
</dl>
</div>

<strong>TWO</strong>
<div id="TWO" class="lambda-exp">
<dl>
<dt><var>f</var></dt>
<dd>
<dl>
<dt><var>x</var></dt>
<dd>
<ol>
<li><var>f</var></li>
<li>
<ol>
<li><var>f</var></li>
<li><var>x</var></li>
</ol>
</li>
</ol>
</dd>
</dl>
</dd>
</dl>
</div>

<strong>THREE</strong>
<div id="THREE" class="lambda-exp">
<dl>
<dt><var>f</var></dt>
<dd>
<dl>
<dt><var>x</var></dt>
<dd>
<ol>
<li><var>f</var></li>
<li>
<ol>
<li><var>f</var></li>
<li>
<ol>
<li><var>f</var></li>
<li><var>x</var></li>
</ol>
</li>
</ol>
</li>
</ol>
</dd>
</dl>
</dd>
</dl>
</div>

<pre>
What good are numbers if you can't add them?
</pre>

<strong>PLUS</strong>
<div id="PLUS" class="lambda-exp">
<dl>
<dt><var>m</var></dt>
<dd>
<dl>
<dt><var>n</var></dt>
<dd>
<dl>
<dt><var>f</var></dt>
<dd>
<dl>
<dt><var>x</var></dt>
<dd>
<ol>
<li><var>n</var></li>
<li>
<ol>
<li><var>f</var></li>
<li>
<ol>
<li>
<ol>
<li><var>m</var></li>
<li><var>f</var></li>
</ol>
</li>
<li><var>x</var>
</ol>
</li>
</ol>
</li>
</ol>
</dd>
</dl>
</dd>
</dl>
</dd>
</dl>
</dd>
</dl>
</div>

<pre>
Since the environment is the DOM, it makes sense that applications
can use variables which exist elsewhere.
</pre>

<strong>Sanity Check our Number System</strong><br />
<button onclick="prelude.compute_toplevel(document.getElementById('SUCC-ZERO-test'))">Reduce</button>
<div id="SUCC-ZERO-test" class="lambda-exp">
<ol>
<li><var>SUCC</var></li>
<li><var>ZERO</var></li>
</ol>
</div>

<button onclick="prelude.compute_toplevel(document.getElementById('SUCC-TWO-test'))">Reduce</button>
<div id="SUCC-TWO-test" class="lambda-exp">
<ol>
<li><var>SUCC</var></li>
<li><var>TWO</var></li>
</ol>
</div>

<button onclick="prelude.compute_toplevel(document.getElementById('PLUS-test'))">Reduce</button>
<div id="PLUS-test" class="lambda-exp">
<ol>
<li>
<ol>
<li><var>PLUS</var></li>
<li><var>TWO</var></li>
</ol>
</li>
<li><var>THREE</var></li>
</ol>
</div>

<strong>Testing variable expansion</strong><br />
<button onclick="prelude.compute_toplevel(document.getElementById('TRUE-test'))">Reduce</button>
<div id="TRUE-test" class="lambda-exp">
Expand Down

0 comments on commit 803c74a

Please sign in to comment.