# Re: [racket-users] Trying to prove a property of a semantics for logic (Prolog-like) programs: could Redex help?

> On Dec 4, 2017, at 9:47 AM, Vincent Nys <vincent...@gmail.com> wrote:
>
> Hi,
>
> I'm currently working on a program transformation technique for logic
> programs. The technique uses abstract interpretation, so I have an abstract
> program semantics and the main operation is an abstraction of resolution. I
> would like to prove a particular property of this semantics (namely that the
> number of non-equivalent abstract conjunctions that can be obtained through
> resolution is finite unless there are recursive calls which can be
> characterized in a specific way). I can't seem to do it by hand. Would Redex
> be of help if I used it to code an interpreter for these abstract semantics?
> I don't necessarily mean that it should produce a complete proof, but, for
> example, could it demonstrate that the property holds for a logic program
> with at most N clauses of length L, where neither is symbolic, by exhausting
> a search space?

Let me first clarify a misunderstanding. Redex is not really a tool for writing
an interpreter. If you want to write interpreters, use Racket or Typed Racket.
Redex is a tool for specifying either a reduction semantics or a relation
semantics. It’s unique for the former and one among others for the latter.

Let me then state a surprising admission. Even though I started as a Prologer
and have always thought of reduction semantics as a unique and amazing tool for
specifying a semantics, I have never done so for a logic language. Interesting.

Now as to your question, Redex can check things but it’s hard to prove them,
even for finite cases. In the past some of my PhD students have developed Redex
model to experiment with a semantics and Isabelle/Coq proofs to prove things.
Modeling in Redex tends to be fast and easy; it really feels like it imposes
only a slightly higher overhead than paper-and-pencil modeling.

Many wish that proof systems and Redex were more integrated. Alas they are not.

— Matthias

--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email