CODEWITHSUNDEEP
clojurelogic-programmingclojure-core.logic
Sebastian Oberhoff
Sebastian Oberhoff

Reputation: 1311

Is there a logical for-all in clojure.core.logic?

I'm trying to solve the first puzzle in Smullyan's To Mock a Mockingbird using clojure.core.logic, not because it is particularly hard, but rather as an exercise. The puzzle states that there's a garden with three colors of flowers: red, yellow, and blue. Each color is present at least once and no matter what three flowers you pick there will be a red and a yellow one among them. Question: is the third necessarily blue?
The basic skeleton of the logic code is quite straightforward:

(run 5 [flowers]
   (counto flowers 3)
   (containso flowers [:red :yellow])
   (fresh [garden]
          (containso garden [:red :yellow :blue])
          (containso garden flowers)
          (forall [flower-selection] (...))))

counto and containso are manually implemented and do the obvious thing. I'm new to this so there might be existing library support that I'm missing. The important line is the one beginning with forall. forall is basically what I wish would exist, but can't seem to find. The only construct I'm aware of that could go in this place is fresh. But fresh essentially performs existential quantification ∃. What I want here is universal quantification ∀.
I'm not interested in a garden for which it is possible to select three flowers which contain a red and a yellow one. I'm interested in a garden which necessarily leads to such a choice.

Upvotes: 3

Views: 262

Answers (1)

amalloy
amalloy

Reputation: 92117

Even if there were a forall, this approach isn't really going to work, because the garden could be arbitrarily large, and to test all combinations of three flowers from an infinite garden will take an infinite amount of time.

And even if you did that, you would still not be done, because you've only proven that there exists one garden which satisfies this property: you haven't proven that all gardens which meet the initial conditions also satisfy the property.

core.logic is "just" a way of modeling search problems that makes it easy to prune subtrees of the search space that are uninteresting. If you are trying to prove a universal statement about an infinite search space, you will need to prune in some way that limits the maximum size of the search space. I don't see any obvious way of doing this in core.logic for this problem, short of thinking some more about the original problem, which will of course lead straight to the solution, without needing core.logic at all.

Upvotes: 2

Related Questions