2019-11-24 10:9:20 (GMT)
Hi Simon
2019-11-24 10:9:56 (GMT)
@Alexander Bentkamp and I have recently discussed some things that might somewhat improve some of the problems that you underlined in the last PR
2019-11-24 10:10:8 (GMT)
Namely, the biggest red flag was something that you correctly pointed out
2019-11-24 10:10:22 (GMT)
and that was the eta-beta reduction that was non-discriminatory
2019-11-24 10:10:38 (GMT)
that is, it ran on all terms regardless whether they contain lambdas or not
2019-11-24 10:11:23 (GMT)
Here is how we propose to fix it efficiently and elegantly:
2019-11-24 10:11:46 (GMT)
Like in E, we will add one new field to the perfectly shared (hashconsed) term
2019-11-24 10:12:26 (GMT)
which is going to keep some of the properties of the term
2019-11-24 10:12:28 (GMT)
for example
2019-11-24 10:12:33 (GMT)
property IsGround
2019-11-24 10:12:44 (GMT)
HasLambdas
2019-11-24 10:12:56 (GMT)
HasCombinators
2019-11-24 10:12:59 (GMT)
etc
2019-11-24 10:13:10 (GMT)
this depends only on the subterms
2019-11-24 10:13:16 (GMT)
so it can be computed very efficiently
2019-11-24 10:13:36 (GMT)
and since we have quite clean interface for constructing terms can be maintained properly
2019-11-24 10:13:41 (GMT)
now
2019-11-24 10:13:44 (GMT)
when we beta reduce
2019-11-24 10:13:54 (GMT)
we check the property HasLambdas (in O(1))
2019-11-24 10:14:40 (GMT)
and if there is a lambda somewhere only then do we eta/beta reduce
2019-11-24 10:14:47 (GMT)
similarly when applying substitution
2019-11-24 10:14:48 (GMT)
if the term is empty
2019-11-24 10:14:53 (GMT)
we leave it as is
2019-11-24 10:14:54 (GMT)
I think
2019-11-24 10:15:1 (GMT)
this might greatly improve the performance of many things
2019-11-24 10:15:29 (GMT)
what we can do further is introduce something like HasBoundVar -- then when we beta reduce we go only in subterms that have bound vars
2019-11-24 10:15:45 (GMT)
what do you think?
2019-11-24 19:21:59 (GMT)
I think it's a good idea. A long time ago I believe there was a bit for "is closed" (wrt De Bruijn indices).
I'd recommend using a mutable flags: int field and bitshifting operations (I can provide examples of similar tricks in OCaml) so that having several fields doesn't make terms too big.
Note that you can compute the flags either at hashconsing, when the term is new; or at first use, if you have a flag for "flags have been computed" (check this one first, then if 0, do the computation).
2019-11-26 12:48:30 (GMT)
Hi Simon I finally see this message
2019-11-26 12:48:35 (GMT)
Ok
2019-11-26 12:48:39 (GMT)
today I will implement some flags
2019-11-26 12:48:51 (GMT)
and they will fix the problem with the order computation
2019-11-26 12:49:15 (GMT)
after that
2019-11-26 12:49:18 (GMT)
we can merge PR
2019-11-26 12:50:22 (GMT)
As for bit shifting
2019-11-26 12:50:42 (GMT)
I am already using Int32 for that in my implementation of the pragmatic version of the unif algorithm
2019-11-26 14:14:46 (GMT)
Uh, please use int if you can, int32 is boxed :(
2019-11-26 14:46:59 (GMT)
The problem with int is that
2019-11-26 14:47:1 (GMT)
as far as I know
2019-11-26 14:48:45 (GMT)
it is machine-dependent
2019-11-26 16:11:27 (GMT)
it's machine dependent, but if you have ≤ 30 bits you're in the clear.
2019-11-26 16:13:54 (GMT)
I am enumerating predicate variables natively -- not using Church encoding of and/or/not/true/false
2019-11-26 16:14:9 (GMT)
but using antive &/|/~/T/F
2019-11-26 16:14:15 (GMT)
it worsk very nice
2019-11-26 16:47:26 (GMT)
That's pretty cool. Another nice thing with combinators is that you can add custom ones for stuff like if then else, or datatype folds, this kind of thing. It makes unification more extensible.
2019-11-26 19:49:33 (GMT)
I implemented cached properties
2019-11-26 19:49:48 (GMT)
now eta/beta is O(1) for terms that need no reduction
2019-11-26 19:50:22 (GMT)
TPTP test on HO problems reveals no problems
2019-11-26 19:50:39 (GMT)
How's the speed on Pelletier problems?
2019-11-26 19:50:48 (GMT)
Did not test
2019-11-26 19:50:55 (GMT)
but it should not influence anything
2019-11-26 19:51:1 (GMT)
since the change
2019-11-26 19:51:10 (GMT)
should only speed up things
2019-11-26 19:51:12 (GMT)
if it is correct
2019-11-26 19:51:17 (GMT)
and this confirms it is