<< Back to previous view

[LOGIC-129] matcha/matchu are not faithful to the semantics of conda/condu Created: 04/Apr/13  Updated: 09/Jun/13

Status: Open
Project: core.logic
Component/s: None
Affects Version/s: None
Fix Version/s: None

Type: Defect Priority: Major
Reporter: Austin Haas Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None


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:

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

;; which has a different meaning than:

  [(== '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]
   [(== '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)

Comment by Austin Haas [ 04/Apr/13 2:35 PM ]

For reference:

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.

From The Reasoned Schemer.

Comment by David Nolen [ 04/Apr/13 5:16 PM ]

Good catch I need to think about this one.

Comment by David Nolen [ 09/Jun/13 12:11 PM ]

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.

Generated at Tue Sep 26 15:05:29 CDT 2017 using JIRA 4.4#649-r158309.