Can ILP learn geometry rules with floating point numbers

[Johnny_Rotten]

@ridgeworks

It was BNR Prolog - for history, see:

Thats exactly where old Prolog ideas have left out, land in
a computer museum, and new Prolog ideas such as λ-Prolog
start, not only the work by @stassa.p but also the Prolog^2

work by James Trewern. While old Prolog ideas have invested
incredible amount of work into this thingy here which waits
for an individual value V, i.e. a value V e D from a first

order theory domain D to arrive:

https://softwarepreservation.computerhistory.org/prolog/#BNR

Delay is only a operational varying interpretation, but its still
a first order interpretation. What 2nd order learning for goals
and clauses basically somehow demands would be:

Where V^2 is a 2nd order variable, with values V^2 e D^2
from a second order domain D^2 so to speak. Here are
some examples, following @stassa.p I drop ^2, you can

identify second order variables by their predicate position:

/* first order */
freeze(X, X > 3)

/* second order */
freeze(Q, Q(3))

Loosly speaking a 2nd order logic can do 2nd order freeze,
since a logic definition itself has no operational definition. It
usually talks about “what” is , and not “how” it is.

But for 2nd order logic MIL, to make it fly, we can either do what
@stassa.p did, look at CONSTRUCT and find that inside the
CONSTRUCT box there is a SLD search. Or we can ask what

is the box itself? What inference rules guard the box itself?

BTW: About the ^2 notation. 2nd order logic uses two sorts
of variables, first order variables V and second order variables V^2.
They belong to two different ontological commitments.

Sometimes it makes it extremly hard to talk about second
order logic, since these ontological commitments are in the
way, for example for the first order natural numbers n e N, that

are countably infinite many, then the predicates P(n) are
uncountably infinite many. But @stassa.p work and others
work doesn’t go that far, its anyways 2nd order quantifier

elimination, turning V^2 variables into V variables somehow.
But who knows, maybe this work will also attract dust, and
land in a computer museum, like λ-Prolog itself. But somehow

I believe a Prolog to Prolog^2 transition is currently in full bloom.

[Johnny_Rotten]

@Johnny_Rotten

But who knows, maybe this work will also attract dust, and
land in a computer museum, like λ-Prolog itself. But somehow

I believe a Prolog to Prolog^2 transition is currently in full bloom.

In as far I somehow belive a Prolog^2 take could be
quite different from a λ-Prolog take. λ-Prolog is still full
of equational reasoning talk, because lambda expressions

and the corresponding higher order unification problem
can be cast as an equational problem. You find that
here in a proof search tutorial, generating a proof

certificate is basically a higher order realization (*):

https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/felty-tutorial-lprolog97.pdf

Since lambda expressions can be cast into an equation
framework, λ-Prolog would fit into the CLP(BNR) take, at
least its praise of equation solving.

But I didn’t hear @stassa.p talk so much about lambda
expressions. His work looks more directed, less creating
an infinite horizon egraph cloud. He even claims polynomial

complexity through his focused method. So I guess this
could be a sign of a paradigmatic shift towards embracing
2nd order variables, but not doing it the λ-Prolog way, but

rather the Prolog^2 way. Still the CONSTRUCT box should
be preferably a well studied white box, and not some black
box, that somewhere calls SLD resolution.

BTW: If one studies the slides by Amy Felty, one finds
that they really have an extrem proof as higher order realizations
stance, adopting lambda expressions. For example a certificate

for a proof of A → A, would be lambda a expression λx.x : A → A,
which matches the Curry Howard isomorphism. But already
combinatorial logic showed that we could have an axiom name

I, which then satisfies the formulae-as-types notion of construction
via I : A → A. Now Prolog^2 and the work of @stassa.p explore
unconsciously some notion of construction via CONSTRUCT.

[Johnny_Rotten]

@ridgeworks

F(X..) =.. [F,X..].

The reason that the freeze/2 for 2nd order functionals is often
a little different than the freeze/2 for 1st order individuals stems
from the idea that one might want to built-in some solving intelligence

into the higher order unification. I guess CLP(BNR) would explicit
use length leveling when it takles the post correspondence
problem (PCP), named after Emil Post, not derived from

HTTP Post, when it would see it as a world algebra problem:

word_algebra({Xs .. } ):- 
    setup_constraints( Xs, SymbolTable), 
    solve_for_lengths(SymbolTable),
    interpret_word_equations(Xs). 

?-word_algebra( { #U =< 3, (-u) & [a] & W & U =(-W) & U & [a] & W}). 

https://softwarepreservation.computerhistory.org/prolog/#BNR

Although the CLP(BNR) paper doesn’t contain a PCP properly. But Dale
Miller has used the PCP, to show that higher order unification is undecidable.
He encodes a PCP as a higher order unification problem:

%  Letters are encoded as functions.  Thus, appending of lists is
%  function composition. (X\ (u (v X))) is a two element
%  list.  (X\X) is the empty list.

/* PCP dominoes: {(uv,vu), (v,vu), (u,e)} */
three_corresp F :-
   (F (X\ (u (v X)))  v             u) =
   (F (X\ (v (u X))) (X\ (v (u X))) (X\X)),

https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/examples/hou/toc.html

Now we find in some lambda Prolog implementation the notion
of elab() elaborating higher order unification constraints. This might
involve something akin to leveling, and is thus mostlikely diverting from

usual Prolog implementation freeze/2 propagation. One finds the notion
elab() already in the Qi dissertation detailing the Teyjus implementation.
And Enrico Tassi also use the notion elab() for his lambda Prolog,

its even a system configuration point which can lead to extensions.
Interestingly bounding the maximum length of a word problem does
not yet imply a leveling, there could be also other strategies, so if

for example @stassa.p would impose some bounds how his 2nd
order templates are expanded, there is still a lot of room how
elaboration(*) during CONSTRUCT is done.

P.S.: (*) Since the word “search” has been banned for the 2nd order MIL
Target Hypothesis Space on request by @stassa.p in relation to CONSTRUCT,
for a while I have used the word “explore”. It need not equal some usual

SLD/freeze. Now I might switch to the HOU jargon “elaborate”.