# Semantics of logic/relational programming languages

I'm working on some vague ideas about a logic/relational programming language based on the linear lambda calculus and having trouble coming up with some appropriate semantics.

If anything the language is more like Prolog than Codd's relational calculus.

For the pure fragment of the language I have some ideas about possible denotational semantics in terms of a list of matching results or a logical relation testing if a term matches. You also ought to be able to compile to a relational algebra or some form of algebraic logic.

I also have some ideas about possible categorical semantics and intend to be able to compile to the category of relations or the category of spans or really any closed monoidal dagger category.

But I'm kind of stuck thinking about other possible semantics. I have an intuition a small step operational semantics ought to be nondeterministic and reduce to any possibly matching term. But this still confuses me.

I've heard about Kripke frame semantics for logics and this kind of seems relevant but I haven't really seen any concrete realizations of this sort of idea for relational languages.

So what are the semantics for relational programming languages?

• Thanks. That's a good place to start. It's slightly awkward to directly work with explicit finite lists of matching values in terms of judgments though. $$E \Downarrow \{ v_1, \ldots , v_n \}$$ is unwieldly. Feb 17 at 3:06