Skip to content

Commit a06a03e

Browse files
committed
Possible fix for counter-example found on stackless algo
The following term: / #f #x /f /f x #A #B #C //B A C Caused the stackless algorithm to behave incorrectly. It halted before reducing all active ports. This patch fixes the algorithm for that specific term, but I'm not sure anymore it works for the same terms that the stack version does. A test suite is necessary.
1 parent 977471e commit a06a03e

File tree

3 files changed

+22
-27
lines changed

3 files changed

+22
-27
lines changed

package.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
{
22
"name": "abstract-algorithm",
3-
"version": "0.1.20",
3+
"version": "0.1.21",
44
"description": "Abstract-algorithm for optional reduction of stratifiable lambda terms",
55
"main": "src/lambda-calculus.js",
66
"bin": {

src/abstract-combinators.js

Lines changed: 20 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -50,23 +50,30 @@ function link(net, a, b) {
5050

5151
function reduce(net) {
5252
var next = net.nodes[0];
53-
var prev, back;
53+
var prev, back, nextMeta, nextSlot;
54+
var i = 0;
5455
while (next > 0) {
5556
prev = enterPort(net, next);
5657
next = enterPort(net, prev);
57-
if (slot(next) === 0) {
58-
if (slot(prev) === 0 && node(prev) !== 0) {
59-
back = enterPort(net, port(node(prev), meta(net, node(prev))));
60-
rewrite(net, node(prev), node(next), net.stats);
61-
next = enterPort(net, back);
62-
} else {
63-
setMeta(net, node(next), 1);
64-
next = enterPort(net, port(node(next), 1));
65-
}
58+
++i;
59+
if (slot(next) === 0 && slot(prev) === 0 && node(prev) !== 0) {
60+
back = enterPort(net, port(node(prev), meta(net, node(prev))));
61+
rewrite(net, node(prev), node(next), net.stats);
62+
next = enterPort(net, back);
6663
} else {
67-
var metaNext = meta(net, node(next));
68-
setMeta(net, node(next), metaNext === 0 ? slot(next) : metaNext + 1);
69-
next = enterPort(net, port(node(next), metaNext === 1 ? 2 : 0));
64+
switch (slot(next) * 3 + meta(net, node(next))) {
65+
case 0 * 3 + 0: nextSlot = 1; nextMeta = 1; break;
66+
case 0 * 3 + 1: nextSlot = 2; nextMeta = 2; break;
67+
case 0 * 3 + 2: nextSlot = 1; nextMeta = 1; break;
68+
case 1 * 3 + 0: nextSlot = 0; nextMeta = 1; break;
69+
case 1 * 3 + 1: nextSlot = 2; nextMeta = 2; break;
70+
case 1 * 3 + 2: nextSlot = 0; nextMeta = 3; break;
71+
case 2 * 3 + 0: nextSlot = 0; nextMeta = 2; break;
72+
case 2 * 3 + 1: nextSlot = 2; nextMeta = 2; break;
73+
case 2 * 3 + 2: nextSlot = 0; nextMeta = 3; break;
74+
}
75+
setMeta(net, node(next), nextMeta);
76+
next = enterPort(net, port(node(next), nextSlot));
7077
}
7178
++net.stats.loops;
7279
}
@@ -110,18 +117,6 @@ function rewrite(net, A, B) {
110117
net.stats.rules += 1;
111118
}
112119

113-
function show(net) {
114-
console.log(net.stats);
115-
for (var i=0; i < net.nodes.length;i+=4) {
116-
if (net.reuse.some(x => x === i>>2)) {
117-
console.log(i>>2);
118-
continue;
119-
}
120-
[a,b,c,d] = net.nodes.slice(i, i+4)
121-
console.log(i>>2, `${a>>2}:${a&3} ${b>>2}:${b&3} ${c>>2}:${c&3} ${d>>2}:${d&3}`);
122-
}
123-
}
124-
125120
module.exports = {
126121
port,
127122
node,

src/lambda-calculus.js

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ const toString = (term, bruijn) => {
7979

8080
const toNet = term => {
8181
var kind = 1;
82-
var net = I.newNet([0, 1, 2, 0]);
82+
var net = I.newNet([0, 2, 1, 4]);
8383
var ptr = (function encode(term, scope){
8484
switch (term.tag){
8585
// Arg

0 commit comments

Comments
 (0)