1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ What does "factored out" mean in this context? $\endgroup$ – cody May 14 '15 at 22:15
  • $\begingroup$ I mean that I want them replaced with my notion of $\top$ . so it's closer to a division or quotient than set removal. $\endgroup$ – David Boshton May 14 '15 at 22:24
  • $\begingroup$ 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? $\endgroup$ – cody May 15 '15 at 2:19
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer May 15 '15 at 8:37
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer May 15 '15 at 8:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.