Thank you for your input. I will look into enlisting a proof assistant.



Op maandag 4 december 2017 19:23:16 UTC+1 schreef Matthias Felleisen:
> > On Dec 4, 2017, at 9:47 AM, Vincent Nys < 
> <javascript:>> 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 
For more options, visit

Reply via email to