2020-01-21 11:45:3 (GMT)
I’d like to share a paper draft with you, which I will submit to FSCD.
The Embedding Path Order for Lambda-Free Higher-Order Terms
Alexander Bentkamp
http://matryoshka.gforge.inria.fr/pubs/epo_paper.pdf
Feedback is very welcome. The deadline for FSCD is Feb 9.
2020-01-21 15:46:53 (GMT)
I will look at that, seems very interesting :-)
2020-01-21 17:21:24 (GMT)
I'm only skimming, but isn't chop ill-typed?
2020-01-21 18:32:30 (GMT)
If there were types, yes, but everything is untyped.
2020-01-21 22:20:42 (GMT)
If there were types, yes, but everything is untyped.
So how does it work in an actual implementation where you do have types? Do you just ignore the typing in the comparison procedure?
2020-01-22 9:28:35 (GMT)
Spelling error on page 1, paragraph 3. "Bhayat and al." should be "Bhayat et al."
2020-01-22 9:35:38 (GMT)
Phew, at first I thought I spelled your name wrong :-). Changed it to "Bhayat and Reger" instead.
2020-01-22 9:39:48 (GMT)
So how does it work in an actual implementation where you do have types? Do you just ignore the typing in the comparison procedure
In Zipperposition, I used a pair (t, [s1, ..., sn]) of a term and a list of terms to stand for t s1 ... sn because Zipperposition would not allow me to construct ill-typed terms.
2020-01-22 16:14:0 (GMT)
Hi Alex!
2020-01-22 16:14:7 (GMT)
I just finished reading your EPO paper
2020-01-22 16:14:9 (GMT)
First of all
2020-01-22 16:14:19 (GMT)
it is written very nicely and it very easy to follow
2020-01-22 16:14:53 (GMT)
I should also point out that I did not read the proofs since it was to no avail because I trust your Isabelle formalization :)
2020-01-22 16:14:57 (GMT)
anyways
2020-01-22 16:15:1 (GMT)
here are some small comments:
2020-01-22 16:15:31 (GMT)
pg.1
2020-01-22 16:15:45 (GMT)
you say:
2020-01-22 16:15:46 (GMT)
. The drawback of this approach is that it is impossible to assign different extension orders such as the lexicographic or multiset extension to different function symbols because the only function symbol in the encoding is @
2020-01-22 16:16:3 (GMT)
this is not entirely true since encoded constants are also function symbols
2020-01-22 16:16:33 (GMT)
the only applied or the only binary function symbol in the encoding is @
2020-01-22 16:16:59 (GMT)
I liked the examples
2020-01-22 16:17:11 (GMT)
but there was one confusing point
2020-01-22 16:31:7 (GMT)
Thank you for the comments, but could you not break your sentences over several messages?
2020-01-22 16:35:51 (GMT)
I hoped you were not receiving them as many notifications :) sorry :)
2020-01-22 16:39:11 (GMT)
I am not. It's just harder to read :grinning: . You can do it if it's more convenient for you...
2020-01-22 16:39:18 (GMT)
On pg. 4. you write
I conjecture that there are no first-order terms comparable with EPO but incomparable with RPO.
However your Example 12. is to the best of my knowledge first-order.
You continue on to say Rules 2 and 3 are not orientable by applicative KBO or applicative RPO.
Maybe a further explanation of how non-applicative RPO deals with this?
2020-01-22 16:39:40 (GMT)
no I am just used to using chat like that :)
I see it can be confusing
2020-01-22 16:40:41 (GMT)
Petar Vukmirovic: the only applied or the only binary function symbol in the encoding is @
Fixed.
2020-01-22 16:43:1 (GMT)
And in the evaluation section you mention how EPO creates the least number of clauses on average.
However, the order is an order of maginture slower than RPO and two orders of magnitude slower than KBO.
Could it be that this is the reason less clauses are created? That is, less conditions can actually be checked,
2020-01-22 16:43:25 (GMT)
and therefore less clauses are created
2020-01-22 16:45:14 (GMT)
Maybe the number of steps can be limited, rather than the timeout?
2020-01-22 16:45:34 (GMT)
One thing that I also missed is that there was no definition of RPO in the paper.
I use KBO all the time, but with RPO (and an instance, if I am not mistaken, LPO) are not so fresh in my memory.
I don't know if you assume that the audience for this paper will be familiar with the orders,
but maybe it would be good to ease the people into it.
2020-01-23 8:55:19 (GMT)
Maybe a further explanation of how non-applicative RPO deals with this?
Fixed.
2020-01-23 9:6:28 (GMT)
Petar Vukmirovic: And in the evaluation section you mention how EPO creates the least number of clauses on average. However, the order is an order of maginture slower than RPO and two orders of magnitude slower than KBO. Could it be that this is the reason less clauses are created? That is, less conditions can actually be checked, and therefore less clauses are created
The average clauses are only computed over those problems that have been solved by all configurations. Therefore it doesn't matter too much that EPO is slower than RPO and KBO. Of course, it might bias the selection of the problems included in the average a bit in the favor of EPO, but I don't think that effect is very strong because you can see for appRPO and appKBO on SH benchmarks that it is possible to produce a lot of clauses and still be very slow.
2020-01-23 9:7:29 (GMT)
Maybe the number of steps can be limited, rather than the timeout?
Maybe. But Starexec will definitely want a timeout in addition.
2020-01-23 9:13:15 (GMT)
One thing that I also missed is that there was no definition of RPO in the paper.
Might be nice, but doesn't really fit into the flow of the paper now. I guess I'll have to live without it.
2020-01-23 9:13:33 (GMT)
Thanks for all the comments, @Petar Vukmirovic !