The Prolog Cabin

« first day (1087 days earlier) ← previous day next day → last day (583 days later) »

8:14 AM

since the prolog chat isn't active i'll post this here. i stumbled upon a comment by the maintainer of clpfd/clpz
> Le Graal de propagation, if we can call it that, will consist in finding a way to generate these propagation rules automatically, ideally starting from a declarative definition of what we mean by "exponentiation" (in this case). Currently, they are only implemented manually, by painstakingly considering the different cases. -- https://github.com/SWI-Prolog/swipl-devel/issues/167#issuecomment-316996913

1 hour later…

user41805

9:29 AM

@user41805 basically the problem is given domains for X, Y, and Z, find their new domains given the condition X op Y #= Z (#= is clpfd's notation for equality)

Bubbler

10:12 AM

@user41805 It is "only" a matter of adding these rules to the library. However, doing so is extraordinarily hard and error-prone - Looks like developing some proofs in, say, Coq will help identify some error-proof rules

user41805

10:39 AM

@Bubbler sure that could be one option

perhaps to get a better idea, here's one example of a failed bounds calculation

failed_lower_bounds([-4..2, -2.. -1, -3.. -2],  (maplist(in, [A, B, C], [-4..2, -2.. -1, -3.. -2]), A*B#=C), [1, -2, -3], [1, -2, -2], [[1, -2, -2], [2, -1, -2]]).

so [-4..2, -2.. -1, -3.. -2] are the domains of [X, Y, Z], the equation is X*Y#=Z, and [1, -2, -3] are the calculated lower bounds for [X,Y,Z] and [1, -2, -2] are the actual lower bounds. [[1, -2, -2], [2, -1, -2]] is just a list of all the actual solutions, whence the actual lower bounds are calculated

and here's the code handling the propagation of multiplication github.com/SWI-Prolog/swipl-devel/blob/master/library/clp/…, note nonvar(X) means X is not a variable meaning it has a fixed integer value as opposed to simply representing a range like 2 .. 5

@user41805 in this example, all X Y and Z are nonvar, so you'd have to look from line 4548 to the end of the predicate

user41805

11:05 AM

so in this case (with nonvar X Y and Z), how would you add a rule/improve the existing rules for better propagation?

currently, separate min_max_factor and min_product and max_product predicates are used, so first the domain of X is restricted considering the domains of Y and Z, then the domain of Y is restricted considering the other two, and then likewise for Z. clearly this is not enough to fully propagate everything, perhaps another cycle of these restrictions would fix it

but another thing to consider is that these mix/max factor/product predicates are used specially for multiplication. for exponentiation, there instead are analogous integer log_b or integer k_th root predicates, obviously generalising would be cooler but that might not be practical

@user41805 "perhaps another cycle of these restrictions would fix it" actually no it doesn't, running with the new constraints again for that specific case did not further change their domains. maybe it does for other examples, but clearly not for this one

that itself might be an interesting question, is it possible to perform these constraint restrictions (i'm probably misusing these terms) only once to get the best set of constraints, or do we need to run over it multiple times?

maybe in this case it's the min_max_factor can be improved, for instance, when the new bounds of the domain Y are being calculated with min_max_factor using the domains of X and Z, it doesn't seem to check whether Z mod Y is 0, to also constrain the domain of Z. perhaps then the propagation of multiplication should be split into a propagation of mod and one of division? or wait, that might end up in an infinite loop

Feeds

11:50 AM

Jo King has unfrozen this room.

Jo King

← 14 messages moved from The Nineteenth Byte

← 1 message moved from The Nineteenth Byte

2 hours later…

user41805

1:29 PM

@user41805 maybe better than constraining Z in min_max_factor would be to do it in min/max_product, which gives the Z limits

another example, so given Z in -3..4, Y in -2..0, X in -4..2, we need to constrain Z. we can obtain the modular equation Z mod Y #= 0, or [-3,4] mod [-2,0] #= 0, and somehow know that Z can't ever be -3, and restrict it to [-2,4]

ah right, -1 can divide [-3,4]

is this even possible?

user41805

2:12 PM

ah wait, it might be as hard as primality testing, --if Z is some prime number and X is 1.. (Z-1) and Y is-- X in 2..99999,Y in 2..99998,X*Y#=65537. already tests for primality

i'm not sure how, but maybe because kill(MState) hasn't yet been triggered

Wezl

2:52 PM

there's a prolog room? great!

user41805

yeah

3 hours later…

user41805

5:53 PM

@Bubbler maybe this is the best solution, would you need to essentially implement prolog in coq? like formal verification

user41805

6:06 PM

i wonder if such libraries already exist

Wezl

unrelated: how do you write full programs in prolog?

I understand how to use write/1 inside of a predicate, but how do I query inside of a file?

do I write a main predicate? So I can just do tpl file.pro

also someone say something funny so all the stars won't be from years ago, please

user41805

@Wezl i don't know, but here's tio.run/##KyjKz8lP1y0uz/z/P00jOb9cU4/LXlchTSMjv6g4FcixAnHA4v//…

Wezl

sorry, I can't access tio.run :( but thanks, I'll go look at some random gh repo

user41805

f(cow).
?- f(horse).
:- f(cow).

Wezl

so putting ?- in a file?

user41805

6:21 PM

actually it doesn't exactly work, :- f(X) doesn't give all the solutions, assuming that's what you wanted. instead take a look at bagof/3 swi-prolog.org/pldoc/doc_for?object=bagof/3 and findall/3,4 swi-prolog.org/pldoc/doc_for?object=findall/3

@Wezl with swi-prolog, you have a goal that takes no arguments (i don't know if it will still work if it takes more than 0 arguments), say run :- write('happy')., then run it with swipl -g run $file_name

so you can give it an other name than run

Wezl

thx, though I still wish there was an easier way (there probably is)

1 hour later…