2019-11-19 16:46:27 (GMT)
Hi Simon!
Did you ever have the code for converting lambda terms to combinators in your
codebase?
Cheers,
Petar
2019-11-19 16:47:52 (GMT)
Yes, there used to be a combinators-based implementation of HO at some point. Look in the history :-)
(I recommend tig or gitg for doing that.)
I imagine you'd want to implement Ahmed's calculus, but I think releasing should come first? I need to take a look at your changes asap.
2019-11-19 16:48:54 (GMT)
Yes. I am implementing Ahmed's calculus :)
Of course. Release is first, but in the meantime I wanted to see what I can do wrt to combinators.
2019-11-19 16:51:0 (GMT)
look at commit 437ff58688fa6cf5ca5ca566f7616f04080df148 , the last one before I removed the combinators code
2019-11-19 16:52:6 (GMT)
ok thx
2019-11-19 16:54:23 (GMT)
I implemented some unification rules and SKIBC combinators.
2019-11-19 16:58:7 (GMT)
ooh unfortunately
it seems like I cannot compile this version :(
2019-11-19 17:0:58 (GMT)
Hmm, what's the error? It's kind of old I guess, might need msat 0.6 or something
2019-11-19 17:1:33 (GMT)
Probably simpler to take the code and copy it into a new branch anyway. The part that defines combinators should definitely be useful.
2019-11-19 17:5:51 (GMT)
I will not use combinatory unification
or even put the combinators in the proof state
2019-11-19 17:7:7 (GMT)
so I will be using them in a completely different context
2019-11-19 17:7:22 (GMT)
I mostly wanted to see if you had any smart tricks that you usually have when it comest
2019-11-19 17:7:29 (GMT)
to
2019-11-19 17:8:26 (GMT)
avoiding repeated occurs checks in the Schoenfinkel conversion algorithm
2019-11-19 17:8:35 (GMT)
(we kind of have to use Schoenfinkel algo)
2019-11-19 17:9:20 (GMT)
Hmm my memory is fuzzy, can you remind me of that?
Also why not use combinators in the proof state? Do you mean you're just going to life functions into combinators at the beginning?
2019-11-20 17:48:26 (GMT)
@Ahmed B came up with a cool calculus that does not need combinators in the proof state.
2019-11-20 17:48:59 (GMT)
What do you need to be reminded of :)
2019-11-20 17:50:23 (GMT)
The Schoenfinkel algo? :p
If you don't have combinators in the proof state, how do you even do unification?!
2019-11-20 18:37:38 (GMT)
There is no need for unification
2019-11-20 18:37:44 (GMT)
You have extra rules that take care of them
2019-11-20 18:37:51 (GMT)
You basically run LFHO unification
2019-11-20 18:53:8 (GMT)
Oh ok, interesting. I'll look at that once it's implemented (unless you can link a paper).
Careful on the lzip-bool branch, there are conflicts again … not sure why
2019-11-20 18:53:19 (GMT)
I tried to address your answers, it looks good!
2019-11-20 19:4:57 (GMT)
tOk
2019-11-20 19:5:2 (GMT)
I will take a look tomorrow
2019-11-20 19:5:7 (GMT)
I am wondering something
2019-11-20 19:5:19 (GMT)
I want to implement combinators in a new module
2019-11-20 19:5:23 (GMT)
in a very extendible manner
2019-11-20 19:5:26 (GMT)
now
2019-11-20 19:5:36 (GMT)
I am wondering how to handle polymorphism of combinators properl
2019-11-20 19:5:38 (GMT)
*properly
2019-11-20 19:6:11 (GMT)
is there code in Zipperposition that is going to calculate the right subsitution for types based on arguments?
2019-11-20 19:6:15 (GMT)
For eaxmple
2019-11-20 19:6:18 (GMT)
look at how it was done in the commit I gave you earlier, really. It just declared the combinators as a bunch of functions.
2019-11-20 19:6:26 (GMT)
yes I saw
2019-11-20 19:6:27 (GMT)
but
2019-11-20 19:6:29 (GMT)
And yes, Term.apply should definitely compute types?
2019-11-20 19:6:48 (GMT)
Yes, but Types.apply expects me to provide the correct type
2019-11-20 19:6:51 (GMT)
for example
2019-11-20 19:7:20 (GMT)
ah, you need to add some unification I guess. It already works this way in inferences.
2019-11-20 19:7:21 (GMT)
if I have S which is of type (A -> B -> C ) -> (A -> B) -> A -> C
2019-11-20 19:8:27 (GMT)
first three arguments of S need to be the types
2019-11-20 19:16:34 (GMT)
Yes, and unification should start by unifying types anyway.
2019-11-20 19:26:19 (GMT)
I now realized that for my needs I will always know the types for each combinator
2019-11-20 19:26:20 (GMT)
thanks anyway
2019-11-20 21:49:21 (GMT)
Ahmed B came up with a cool calculus that does not need combinators in the proof state.
What do you mean by 'in the proof state'?
2019-11-26 12:58:4 (GMT)
I think they mean having the clauses s X Y Z = X Z (Y Z), k X Z = X etc in the clause set.
2019-11-26 14:15:53 (GMT)
Oh? If that's the case, what I wrote didn't have that either (it was rewrite rules, not clauses, and the paramodulation with rules was acting like HO unif)
2019-11-26 14:47:26 (GMT)
Ok, then it's similar to what you had, except that Ahmed's calculus uses only lambda-free unification
2019-11-26 14:50:13 (GMT)
(it was rewrite rules, not clauses, and the paramodulation with rules was acting like HO unif)
If I understand the above correctly, @Simon Cruanes 's calculus also utilised first-order unification? The main difference appears to be that I can (hopefully) provide a completeness guarantee if the correct ordering is used!
2019-11-26 16:13:7 (GMT)
If I understand the above correctly, Simon Cruanes 's calculus also utilised first-order unification? The main difference appears to be that I can (hopefully) provide a completeness guarantee if the correct ordering is used!
No, I used applicative unification (i.e. there were no lambdas, but there were head variables already). And narrowing (rather than paramodulation, sorry) with the combinators left-to-right rules to emulate HO unification. I also had some boolean combinators to emulate enumeration of predicate variables :wink:
2019-11-26 16:13:26 (GMT)
But yeah, there was no completeness guarantee.
2019-11-26 17:50:49 (GMT)
If I understand the above correctly, Simon Cruanes 's calculus also utilised first-order unification? The main difference appears to be that I can (hopefully) provide a completeness guarantee if the correct ordering is used!
No, I used applicative unification (i.e. there were no lambdas, but there were head variables already). And narrowing (rather than paramodulation, sorry) with the combinators left-to-right rules to emulate HO unification. I also had some boolean combinators to emulate enumeration of predicate variables :wink:
That is more-or-less what I do (other than boolean combinator part). Internally, Vampire stores all applicative terms using the (in)famous binary app function and therefore applicative unification becomes standard first-order unification.
I'm interested in these if-then-else combinators. Could you explain a bit further? Thanks
2019-11-26 18:31:45 (GMT)
I think it was something like If x f1 f2 y z with
If true f1 f2 y z = f1 y and
If false f1 f2 y z = f2 z, or even just the basic If x y z, can't remember.
2019-11-26 18:32:41 (GMT)
The idea is that you can synthesize terms that contain if using such combinators and regular unification.
Similar idea for fold_nat : (a -> a) -> a -> nat -> a (a combinator that converts a natural number datatype into its Church representation).