2
$\begingroup$

I have a [finite] lattice enriched with additional operations. I would like either:

  1. find a pair of binary operations (and constants) satisfying semiring laws, or
  2. prove that no such operations exist

As the structure is finite, one can approach problem #1 via computerized search. For illustration purpose if I had boolean algebra with operations $\vee$, $\wedge$, and $\neg$, then the search would return semiring operations $\oplus$ and $\otimes$ expressed via those. However, if this search fails, how would I prove that no such operations exist?

I assume that there are fundamental properties of semirings, that can be employed. By "fundamental" I mean that they don't explicitly refer to semiring operations; they only assume that such operations exist. Therefore, one just have to show that my lattice doesn't possess those. So what are fundamental properties of semirings?

Edit: to give a justification why I suspect semiring structure can exist is that my lattice is in many respects is similar to relation algebra. Unfortunately, what might be considered the intuitive analogous of composition operation is not associative. Yet, the structure contains more than one instance of everything: there are two conjunction, two disjunctions, two negations, and four constants, so there might be more than one way to manufacture composition.

Improve this question
$\endgroup$
5
  • $\begingroup$ What relations must there be between the semiring structure and the structures you already have? Or is the problem just to impose a semiring operation on a finite set? $\endgroup$
    – Jack Huizenga
    Commented Nov 28, 2011 at 22:05
  • $\begingroup$ To give another analogy, suppose you have just discovered natural numbers but addition and multiplication yet are not known. For example, all we have are binary GCD, LCM and, say, unary increment. One can proceed "discovering" standard addition and multiplication (I assume those are expressible via GCD, LCM, and increment or, assume more esoteric operations if this is not the case) $\endgroup$
    – Tegiri Nenashi
    Commented Nov 28, 2011 at 22:52
  • $\begingroup$ We still want to know how the lattice is supposed to be related to the semiring, beyound just being defined on the same underlying set... $\endgroup$
    – darij grinberg
    Commented Nov 28, 2011 at 23:19
  • $\begingroup$ I don't understand the repeated calls for relation between lattice and semiring. Can you explain it on the example of boolean algebra? If one have BA with lattice structure, he could just discover that (with some incidental choice of operations) it's also a semiring. I just fail to see beyond the formulas which express multiplication and addition in terms of conjunction, disjunction, and negation... $\endgroup$
    – Tegiri Nenashi
    Commented Nov 28, 2011 at 23:29
  • $\begingroup$ The point people are making is that if you don't want a relationship between the lattice structure and the semiring structure, then you might as well forget the lattice structure and ask whether the set admits a semiring structure. It sounds like you want the semiring operations to be derivable from the lattice ones. This question is to vague to get a good answer. $\endgroup$
    – Benjamin Steinberg
    Commented Nov 29, 2011 at 0:04

1 Answer 1

Reset to default
4
$\begingroup$

I will interpret your question to mean:

Is there a small (closed-form) expression in the existing symbols in my algebraic structure which can be interpreted as $\oplus$ and $\otimes$ for a semiring?

Of course, this also assumes you have candidates for $0$ and $1$. I would use the finite model verifier Mace4 for this. If you want to see a nice example of this technique in action, I recommend Modal semirings revisited by Desharnais and Struth. They use both Prover9 and Mace4 for finding structures and disproving that some exist, in a very similar domain to yours. P.14 of that paper even shows some sample input for those programs to get the kinds of results you want. Another place to look is this repository of Prover9 files.

Improve this answer
$\endgroup$
1
  • $\begingroup$ I was not aware that Mace4 is capable beyond finding axiom redundancy and inconsistency, thank you. $\endgroup$
    – Tegiri Nenashi
    Commented Nov 29, 2011 at 2:10

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .