I would expect "y" to remain unbound, as in "not enough information". When evaluated, the "if" expression is added to the "knowledge store", so that it will be

I would expect "y" to remain unbound, as in "not enough information". When evaluated, the "if" expression is added to the "knowledge store", so that it will be evaluated when "x" is bound elsewhere, giving "y" the corresponding value (just "1" or just "2", never "(1|2)") only after that. P.S. See the definition of the "amb" operator in typical logic programming languages: https://rosettacode.org/wiki/Amb https://rosettacode.org/wiki/Amb