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…
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)

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

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

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

11:50 AM
Jo King has unfrozen this room.

14 messages moved from The Nineteenth Byte
1 message moved from The Nineteenth Byte

2 hours later…
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?

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

2:52 PM
there's a prolog room? great!

yeah

3 hours later…
5:53 PM
@Bubbler maybe this is the best solution, would you need to essentially implement prolog in coq? like formal verification

6:06 PM
i wonder if such libraries already exist

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
2

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

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

so putting `?-` in a file?

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`

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

1 hour later…
7:38 PM
@Wezl I have obliged (or rather, you have)
@Wezl This question seems to be similar - an answer suggests using `initialization`

trealla seems to ignore it, though
oh, now it's working
though the prompt still shows up, even if my initialization includes halt.