4
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

A good place to start might be Datalog which has various clean approaches to semantics. A Datalog program is (simplifying a bit) a function-free and negation-free Prolog program.

For the semantics of Datalog see [1], but the idea is simple: a predicate denotes the set of tuples that satisfy it. Compared to Prolog, one of the key restrictions Datalog imposes is that these sets are always finite. This helps keep proof search decidable, allowing for a variety of implementation strategies.

  1. S. Ceri, G. Gottlob, L. Tanca, What You Always Wanted to Know About Datalog (and Never Dared to Ask).
Improve this answer
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Ms. Molly Stewart-Gallus
    Commented Feb 17, 2022 at 3:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.