<p>In the context of <a href="http://en.wikipedia.org/wiki/Cartesian_closed_category" rel="nofollow">CCC</a>, your transformation is interpreted as “$mb:A\to B, mc:A\to C$ is transformed to $\langle mb, mc \rangle : A\to B\times C$”, i.e. the <a href="http://en.wikipedia.org/wiki/Product_(category_theory)" rel="nofollow">product of morphisms</a>.</p>

CC BY-SA 2.5
2010-12-31T12:45:35.400Z
2010-12-31T12:45:35.400Z
beroal
<p>So, this is an instance of the fact that $(A \supset B) \wedge (A \supset C)$ is equivalent to $A \supset (B \wedge C)$. A different type isomorphism, namely that $(B \supset A) \wedge (C \supset A)$ is equivalent to $(B \vee C) \supset A$, looks more like what you wrote down, but that's because in logic programming notation we write B :- A when we mean $A \supset B$. (Note: $\supset$ is "implies," $\wedge$ is "and," and $\vee$ is "or.")</p>

<p>What you're trying to do is related to the <i>binarization</i> transformation, which is discussed in McAllester's "On the complexity analysis of static analyses." There may be a better name for the transformation, but if so, it wasn't known the authors of the paper "<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.2025">A succinct solver for ALFP</a>" (<b><i>A</i></b>lternating <b><i>L</i></b>east <b><i>F</i></b>ixed<b><i>p</i></b>oint formulas are a generalization of Horn clauses for bottom-up logic programs such as yours) - in Example 1 on page 4 they discuss a similar transformation and just call it "exploiting the possibility of sharing of pre-conditions."</p>

CC BY-SA 2.5
2010-12-07T03:52:41.793Z
Man, I have got to stop shallow parsing whole fields of research, and getting my education from Wikipedia. Maybe then I can find out what the wheel is called *before* I reinvent it. (But first I need to finish my PhD o.O)
badroit
CC BY-SA 2.5
2010-12-07T09:28:26.120Z
Sorry for my wrong answer. I shouldn't post late in the evening.
Dave Clarke
CC BY-SA 2.5
2010-12-07T19:13:03.667Z
I understand the feeling (applies to both comments!)
Rob Simmons
CC BY-SA 2.5
2010-12-07T00:33:38.793Z
2010-12-07T12:01:11.873Z
2010-12-07T12:01:11.873Z
Rob Simmons
<p>I hope I've come to the right place... it's (probably) a fairly straightforward Logic Programming question.</p>

<p>If I have two clauses of the form:
<code>B:-A C:-A</code>
I can transform these into:
<code>B,C:-A</code></p>

<p>(<strong>Edit:</strong> <em>where <code>B,C</code> is a conjunction. I'm doing bottom-up evaluation and it's useful to me to represent multiple clauses with the same body using one clause with a conjunction of the respective heads. This seems trivial, but I'm wondering if there's a name for such a transformation&mdash;however, I know that the resulting clause is no longer a Horn clause.</em>)</p>

<p>Does anyone know if this transformation has a name, and if so, can anyone provide a pointer (preferably online) to somewhere that describes it.</p>

<p>Many thanks (from a n00b).</p>

<reference-request><pl.programming-languages><terminology><logic-programming>
Logic Programming: Transforming B:-A C:-A to B,C:-A
badroit
# Logic Programming: Transforming B:-A C:-A to B,C:-A

(Asked by: username_0 on 2010-12-06)

I hope I've come to the right place... it's (probably) a fairly straightforward Logic Programming question.

If I have two clauses of the form:
`B:-A C:-A`
I can transform these into:
`B,C:-A`

(**Edit:** *where `B,C` is a conjunction. I'm doing bottom-up evaluation and it's useful to me to represent multiple clauses with the same body using one clause with a conjunction of the respective heads. This seems trivial, but I'm wondering if there's a name for such a transformation—however, I know that the resulting clause is no longer a Horn clause.*)

Does anyone know if this transformation has a name, and if so, can anyone provide a pointer (preferably online) to somewhere that describes it.

Many thanks (from a n00b).

**Tags:** reference-request, pl.programming-languages, terminology, logic-programming

---

## 2 answers

### Answer by username_2 on 2010-12-07. Score: 8 | Accepted answer

So, this is an instance of the fact that $(A \supset B) \wedge (A \supset C)$ is equivalent to $A \supset (B \wedge C)$. A different type isomorphism, namely that $(B \supset A) \wedge (C \supset A)$ is equivalent to $(B \vee C) \supset A$, looks more like what you wrote down, but that's because in logic programming notation we write B :- A when we mean $A \supset B$. (Note: $\supset$ is "implies," $\wedge$ is "and," and $\vee$ is "or.")

What you're trying to do is related to the *binarization* transformation, which is discussed in McAllester's "On the complexity analysis of static analyses." There may be a better name for the transformation, but if so, it wasn't known the authors of the paper "[A succinct solver for ALFP](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.2025)" (***A***lternating ***L***east ***F***ixed***p***oint formulas are a generalization of Horn clauses for bottom-up logic programs such as yours) - in Example 1 on page 4 they discuss a similar transformation and just call it "exploiting the possibility of sharing of pre-conditions."

> **Comments:**
> **username_0**: Man, I have got to stop shallow parsing whole fields of research, and getting my education from Wikipedia. Maybe then I can find out what the wheel is called *before* I reinvent it. (But first I need to finish my PhD o.O)  
> **username_3**: Sorry for my wrong answer. I shouldn't post late in the evening.  
> **username_2**: I understand the feeling (applies to both comments!)  

---

### Answer by username_1 on 2010-12-31. Score: 2

In the context of [CCC](http://en.wikipedia.org/wiki/Cartesian_closed_category), your transformation is interpreted as “$mb:A\to B, mc:A\to C$ is transformed to $\langle mb, mc \rangle : A\to B\times C$”, i.e. the [product of morphisms](http://en.wikipedia.org/wiki/Product_(category_theory)).


---

