Welcome! Please see the About page for a little more info on how this works.

0 votes
in core.logic by

The semantics of conda and condu give special importance to the head of each clause, but the pattern matching macros in core.logic that are built on top of them merge the body into the head. That means that every expression in a body position is considered when deciding which line is chosen, rather than just the expression in the head position. This is because the entire clause is wrapped in a fresh expression to bind the implicitly specified lvars that appear in the pattern.

To illustrate:

`
(matcha ['a]

[['a] u#]
[['a] s#])

;; expands to:

(conda
[(fresh [] (== 'a 'a) u#)]
[(fresh [] (== 'a 'a) s#)])

;; which has a different meaning than:

(conda
[(== 'a 'a) u#]
[(== 'a 'a) s#])

`

Ideally, we could devise a new system to marry the semantics of conda with pattern matching. At the very least, I think the offending macros should carry a warning in their docstring, stating this semantic difference.

I suspect this would also cause the "Third Commandment" warning to apply to the entire line, rather than just the head/question, but I have not investigated that issue.

Here's an example that demonstrates the difference in meaning:

`
;; This does not succeed, because we commit to the first line,
;; since the question succeeds, but then fail in the body.

(run* [q]
(conda
[(== 'a 'a) u#]
[(== 'a 'a) s#]))

;; => ()

;; This succeeds, because the whole line is used to determine which line to commit to,
;; rather than just the pattern matching clause at the head. So when the first line fails,
;; the second line is tried.

(run* [q]
(matcha ['a]
[['a] u#]
[['a] s#]))

;; => (_0)
`

4 Answers

0 votes
by

Comment made by: austinhaas

For reference:

{quote}

The Third Commandment

If prior to determining the question of a conda (or condu) line a variable is fresh, it must remain fresh in the question of that line.
{quote}

From The Reasoned Schemer.

0 votes
by

Comment made by: dnolen

Good catch I need to think about this one.

0 votes
by

Comment made by: dnolen

The issue is that we rely on the conde macro which isn't very flexible. We should probably do something one step lower so can wrap each conde line in a let that constructs the logic vars and then ensure that all the head unifications are wrapped in one fresh so that the semantics of conda/u are preserved.

0 votes
by
Reference: https://clojure.atlassian.net/browse/LOGIC-129 (reported by austinhaas)
...