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

2017-12-05 Thread Vincent Nys 
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  
> 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  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 racket-users...@googlegroups.com .
> 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 racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

2017-12-04 Thread Vincent Nys 
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  > 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 racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

2017-12-04 Thread Matthias Felleisen 

> On Dec 4, 2017, at 9:47 AM, Vincent Nys  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 racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

2017-12-04 Thread Vincent Nys 
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?

Thanks in advance,

Vincent

-- 
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 racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.