Investigating samples/counter.mlc against encoding/abstract

[Mathnerd314]

Hi, I saw from the thread on LtU that the proposed impure/fast algorithm was not working on a big example counter.mlc. Is that still the case? I was thinking about investigating it with the GUI from http://hackage.haskell.org/package/graph-rewriting-lambdascope

[codedot]

Yes, that is still the case:

(f: f (f (x: x))) (i: (f: f (x: x) (f (x: x))) (x: (h, u: h (h u)) (y: x (i y))))

is reduced to v1: v1 by closed, optimal (Lambdascope-like), and standard (Asperti-and-Guerrini-like), while making abstract fail as follows after 34 interaction steps:

$ npm i -g @alexo/lambda
+ @alexo/lambda@0.5.1
updated 7 packages in 4.897s
$ lambda -f samples/counter.mlc -a optimal -pt
(f: f (f (x: x))) (i: (f: f (x: x) (f (x: x))) (x: (h, u: h (h u)) (y: x (i y))))
582(14), 4 ms
v1: v1
$ lambda -f samples/counter.mlc -d
[...]
NO RULES: !print = \fanout_{5}(w1, w2);
$ 

Investigating the counterexample would be of great help. Thanks a lot!

[Mathnerd314]

I made some progress drawing graphs: (First is this repo's Lambdascope + graphviz dot, second is the Haskell Lambdascope using force-directed layout). Next step is to run the abstract algorithm and try to find the problem.

[codedot]

I just realized that the following information might be useful in investigation.

By adding some debug output:

diff --git a/encoding/abstract/template.txt b/encoding/abstract/template.txt
index 27b2b6b..a6ac35b 100644
--- a/encoding/abstract/template.txt
+++ b/encoding/abstract/template.txt
@@ -17,6 +17,7 @@
 \fanin_{i}[\fanout_{this.phi(j, i)}(a, b), \fanout_{j}(c, d)] {
 	/* Duplicate different fans. */
 	if (!this.match(i, j))
+		console.log("%s><%s -> %s<>%s", i, j, this.phi(j, i), this.phi(i, j)),
 		++this.total;
 	else
 		return false;
@@ -25,6 +26,7 @@
 \fanin_{i}[a, b] {
 	/* Annihilate matching fans. */
 	if (this.match(i, j))
+		console.log("%s><%s", i, j),
 		++this.total;
 	else
 		return false;
diff --git a/encoding/optimal/template.txt b/encoding/optimal/template.txt
index 9d054d3..492c538 100644
--- a/encoding/optimal/template.txt
+++ b/encoding/optimal/template.txt
@@ -105,6 +105,7 @@
 \fan_{i}[a, b] {
 	/* Annihilate matching fans. */
 	if (i == j)
+		console.log("%s><%s", i, j),
 		++this.total;
 	else
 		return false;
@@ -113,6 +114,7 @@
 \fan_{i}[\fan_{j}(a, b), \fan_{j}(c, d)] {
 	/* Duplicate higher fan. */
 	if (i < j)
+		console.log("%s><%s -> %s<>%s", i, j, j, i),
 		++this.total;
 	else
 		return false;

it is possible to compare fan interactions between optimal and abstract against samples/counter.mlc, taking into account that the abstract algorithm is intended to make fans behave the same way (with respect to duplication and annihilation) as if oracle were still present:

	OPTIMAL			ABSTRACT
	1><3 -> 3<>1		3><2 -> 2<>4
	4><4			2><2
	2><4 -> 4<>2		2><1 -> 1<>5
	2><6 -> 6<>2		3><1 -> 1<>6
	7><7			1><1
	1><4 -> 4<>1		1><3 -> 6<>1
(1)	2><4 -> 4<>2		5><6 -> 6<>7
	2><2			6><6
	4><6 -> 6<>4		1><2 -> 5<>1
	5><5			5><5
	7><7			1><1
	4><6 -> 6<>4		1><2 -> 5<>1
(2)	5><5			7><5 -> 5<>8
	2><6 -> 6<>2		2><5 -> 5<>9
	9><9			3><5 -> 5<>10
	2><2			
	7><7			
	8><8			
	8><10 -> 10<>8			
	8><8			
	11><11			
	11><11			
	8><8						

Thus step (2) is clearly wrong. Further looking into the indices and where they come from suggests that the error might be due to step (1) where fan with index 7 is created. It seems that fans 5 and 6 should have inherited relation between their prototypes 2 and 3 in some sense. The latter idea is supported by the following experiment:

diff --git a/encoding/abstract/template.txt b/encoding/abstract/template.txt
index a6ac35b..7c4bb62 100644
--- a/encoding/abstract/template.txt
+++ b/encoding/abstract/template.txt
@@ -71,7 +71,7 @@ $$
 
 READBACK
 
-const map = new Map();
+const map = new Map([["5,6", 5], ["6,5", 7]]);
 let nonce = 0;
 
 function decide(i, j)

which in turn results in the following comparison:

	OPTIMAL			ABSTRACT-HACK
	1><3 -> 3<>1		3><2 -> 2<>4
	4><4			2><2
	2><4 -> 4<>2		2><1 -> 1<>5
	2><6 -> 6<>2		3><1 -> 1<>6
	7><7			1><1
	1><4 -> 4<>1		1><3 -> 6<>1
(1')	2><4 -> 4<>2		5><6 -> 7<>5
	2><2			6><6
	4><6 -> 6<>4		1><2 -> 5<>1
	5><5			5><5
	7><7			1><1
	4><6 -> 6<>4		1><2 -> 5<>1
(2')	5><5			5><5
	2><6 -> 6<>2		4><1 -> 1<>7
	9><9			1><1
	2><2			7><7
	7><7			1><1
	8><8			1><1
	8><10 -> 10<>8		2><3 -> 4<>2
	8><8			3><3
	11><11			2><2
	11><11			2><2
	8><8			4><4

where step (1') is swapped compared to (1) which makes step (2') annihilation instead of duplication (2).

[Mathnerd314]

I read your papers but I still don't really understand the semantics. In particular, the main goal of optimal reduction is to evaluate a lambda term - hence, the graph always represents some lambda term The BOHM algorithm and Lambdascope both give correctness arguments based on tracing paths from the root with a context/stack semantics to produce an explicit lambda term at each step. Are there any similar semantics for your algorithm? The embedded read-back stuff you have just seems to work for normal forms, it doesn't give an in-progress lambda term.

[codedot]

It is true that the embedded read-back mechanism can only retrieve the β-normal form of a term (if any). As for keeping track of the evaluated term during reduction, it should be possible the same way as in BOHM and Lambdascope. At least, the intention is that the experimental algorithm keeps the interaction net structurally identical to those of the abstract version of Lamping's algorithm as well as BOHM and Lambdascope with brackets/croissants and delimiters removed, respectively.