<p>Major rewrite justifiably asked for:</p>

<p>I'm currently trying to get a categorical way of doing something called the Gelfond-Lifschitz reduct on a set of single-headed Horn clauses. The semantics is the answer set semantics, and the idea is that given a program </p>

<p>$\Pi=\{a_i\gets L_{i_1}, \dots L_{i_k}, i\in\{1\dots n\}\}$ and a model $S$,</p>

<p>the Gelfond Lifschitz reduct on $\Pi$ is $\Pi$ with the following removed:</p>

<ol>
<li>All occurences of clauses with $not\ a$ in the body for $a\in S$</li>
<li>All occurences $not\ a$ for all $a\notin S$.</li>
</ol>

<p>Now, having a basic games model of this already, I'm trying to find out what further contraints on the category of games are required.</p>

<p>A seemingly neat way of doing the first part of the G-L reduct is being able to factor out points denoted by the model $S$ from the object denoting $\Pi$ such that every map in the denotation of $\Pi$ containing a map to the terminal object should be removed. (denoting negation as a map to the terminal object)</p>

<p>Similarly the second part requires a similar construct, where everything not consisdered a point by the denotation of the model should be removed entirely from the object denoted by $\Pi$.</p>

<p>I hope this makes more sense and I am very willing to clarify more.</p>

<p><strong>More Clarification:</strong></p>

<p>To summarize the semantics, we take a program $\Pi$ and denote that it itself is a category with objects as the literals and the horn clauses are the maps. We define a few operations on the category $C_{\Pi}$ denoting $\Pi$, namely the transitive closure as well as satisfiable model map which takes $C_{\Pi}$ to a category whose objects are purely points. </p>

<p>The point is that I have two effective issues at the same time. I need a semantics that allows the literals to be objects and the general denotation of implication to be a map between objects, <em>and</em> I need a set of operations on the categories denoted by the programs to constrain the categories.</p>

CC BY-SA 3.0
2015-05-14T22:15:13.077Z
What does "factored out" mean in this context?
cody
CC BY-SA 3.0
2015-05-14T22:24:53.420Z
I mean that I want them replaced with my notion of $\top$ . so it's closer to a division or quotient than set removal.
David Boshton
CC BY-SA 3.0
2015-05-15T02:19:34.133Z
What is $\top$ in this context? What does it mean to "replace them"? We need some more background on this question: what is your ultimate goal here?
cody
CC BY-SA 3.0
2015-05-15T08:37:20.523Z
Voting to close in order to motivate the author of the question to ask his question in such a way that we will understand him.
Andrej Bauer
CC BY-SA 3.0
2015-05-15T08:38:55.843Z
Given a category $\mathcal{C}$ and an object $X$ in it, you can always "take out" the object $X$ by forming the full subcategory on all the objects except $X$. You could also throw out all isomorphic copies of $X$. But I am guessing this is not what you want.
Andrej Bauer
CC BY-SA 3.0
2015-05-15T08:39:52.877Z
Rather than asking for something in category theory, it might be better to explain what sort of semantics you're looking for.
Andrej Bauer
CC BY-SA 3.0
2015-05-15T11:31:28.467Z
Could you say a bit more about how your categorical semantics works so far. What is $\Pi$ in the semantics, an object? Why do you need categories anyway? Can't you just do everything with sets?
Andrej Bauer
CC BY-SA 3.0
2015-05-20T21:01:01.103Z
@AndrejBauer I've added some more, I hope this helps. Currently the operation I'm looking for at a level higher than that of objects denoting literals and implications denoting maps. Does that make sense?
David Boshton
CC BY-SA 3.0
2015-05-20T21:23:40.070Z
It's not clear to me at all why you need categories, and in any case your definition of the category is not clear, how does composition work, where do identity morphisms come from? Also, I think I do not understand the terminology. If  the objects of your category are literals, then how can an implication $a_i \leftarrow L_i$ be a morhism when $L_i$ is a conjunction of *several* literals? At best this could be a multicategory, or there's something basic I misunderstand here.
Andrej Bauer
CC BY-SA 3.0
2015-05-21T09:10:03.420Z
I am probably wrong, knowing not enough about category theory, but I thought I can add a product and coproduct structure to the category. You are right; the product of many literals is an allowable object in each category.
David Boshton
<ct.category-theory><denotational-semantics>
Categorical way of factoring out points
David Boshton
# Categorical way of factoring out points

(Asked by: username_0 on 2015-05-14)

Major rewrite justifiably asked for:

I'm currently trying to get a categorical way of doing something called the Gelfond-Lifschitz reduct on a set of single-headed Horn clauses. The semantics is the answer set semantics, and the idea is that given a program

$\Pi=\{a\_i\gets L\_{i\_1}, \dots L\_{i\_k}, i\in\{1\dots n\}\}$ and a model $S$,

the Gelfond Lifschitz reduct on $\Pi$ is $\Pi$ with the following removed:

1. All occurences of clauses with $not\ a$ in the body for $a\in S$
2. All occurences $not\ a$ for all $a\notin S$.

Now, having a basic games model of this already, I'm trying to find out what further contraints on the category of games are required.

A seemingly neat way of doing the first part of the G-L reduct is being able to factor out points denoted by the model $S$ from the object denoting $\Pi$ such that every map in the denotation of $\Pi$ containing a map to the terminal object should be removed. (denoting negation as a map to the terminal object)

Similarly the second part requires a similar construct, where everything not consisdered a point by the denotation of the model should be removed entirely from the object denoted by $\Pi$.

I hope this makes more sense and I am very willing to clarify more.

**More Clarification:**

To summarize the semantics, we take a program $\Pi$ and denote that it itself is a category with objects as the literals and the horn clauses are the maps. We define a few operations on the category $C\_{\Pi}$ denoting $\Pi$, namely the transitive closure as well as satisfiable model map which takes $C\_{\Pi}$ to a category whose objects are purely points.

The point is that I have two effective issues at the same time. I need a semantics that allows the literals to be objects and the general denotation of implication to be a map between objects, *and* I need a set of operations on the categories denoted by the programs to constrain the categories.

**Tags:** ct.category-theory, denotational-semantics

> **Comments:**
> **username_1**: What does "factored out" mean in this context?  
> **username_0**: I mean that I want them replaced with my notion of $\top$ . so it's closer to a division or quotient than set removal.  
> **username_1**: What is $\top$ in this context? What does it mean to "replace them"? We need some more background on this question: what is your ultimate goal here?  
> **username_2**: Voting to close in order to motivate the author of the question to ask his question in such a way that we will understand him.  
> **username_2**: Given a category $\mathcal{C}$ and an object $X$ in it, you can always "take out" the object $X$ by forming the full subcategory on all the objects except $X$. You could also throw out all isomorphic copies of $X$. But I am guessing this is not what you want.  
> **username_2**: Rather than asking for something in category theory, it might be better to explain what sort of semantics you're looking for.  
> **username_2**: Could you say a bit more about how your categorical semantics works so far. What is $\Pi$ in the semantics, an object? Why do you need categories anyway? Can't you just do everything with sets?  
> **username_0**: @AndrejBauer I've added some more, I hope this helps. Currently the operation I'm looking for at a level higher than that of objects denoting literals and implications denoting maps. Does that make sense?  
> **username_2**: It's not clear to me at all why you need categories, and in any case your definition of the category is not clear, how does composition work, where do identity morphisms come from? Also, I think I do not understand the terminology. If  the objects of your category are literals, then how can an implication $a_i \leftarrow L_i$ be a morhism when $L_i$ is a conjunction of *several* literals? At best this could be a multicategory, or there's something basic I misunderstand here.  
> **username_0**: I am probably wrong, knowing not enough about category theory, but I thought I can add a product and coproduct structure to the category. You are right; the product of many literals is an allowable object in each category.  

---

## 0 answers

