So many reasons to dig into things I've wanted to look at for a while! Op dinsdag 5 december 2017 18:23:37 UTC+1 schreef Matthias Felleisen: > > > You may also wish to look into Rosette, a Racket-based SMT DSL. Emina > Torlak is the creator and you should be able to find it from her web site — > Matthias > > > > > On Dec 5, 2017, at 1:37 AM, Vincent Nys <[email protected] <javascript:>> > wrote: > > Matthias, > > Thank you for your input. I will look into enlisting a proof assistant. > > Regards, > > Vincent > > Op maandag 4 december 2017 19:23:16 UTC+1 schreef Matthias Felleisen: >> >> >> > On Dec 4, 2017, at 9:47 AM, Vincent Nys <[email protected]> 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 to [email protected] <javascript:>. > For more options, visit https://groups.google.com/d/optout. > > >
-- 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 to [email protected]. For more options, visit https://groups.google.com/d/optout.
