[racket-users] Re: dynamically creating and traversing slides
Went for a walk and had an idea. I think this sample illustrates the answer to my own question: #lang slideshow (define (retract-up-to s retracted) (let ([newly-retracted (retract-most-recent-slide)]) (if (eq? newly-retracted s) (cons newly-retracted retracted) (retract-up-to s (cons newly-retracted retracted) (slide #:title "Slide 1") (slide #:title "Slide 2") (slide #:title "Slide 3") (slide #:title "Branching slide" (clickback (t "1") (λ () (let* ([remainder (retract-up-to remainder-start (list))] [branch-start #f] [_ (begin (slide #:title "1" (clickback (t "a") (λ () (slide #:title "a" (clickback (t "resume remainder") (λ () (retract-up-to branch-start '()) (re-slide (car remainder)) (start-at-recent-slide) (for ([rem-sl (cdr remainder)]) (re-slide rem-sl) (start-at-recent-slide (set! branch-start (most-recent-slide)))]) (start-at-recent-slide) (define branching-slide (most-recent-slide)) (slide #:title "Remainder 1") (define remainder-start (most-recent-slide)) (slide #:title "Remainder 2") (slide #:title "Remainder 3") -- 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] dynamically creating and traversing slides
Hi, I'm working on some lecture slides and I'd like my students to list some examples. My idea was to have a few question marks on my slides that I would click to reveal the example whenever someone calls it out. But I'm stuck, because while I can add a slide at the end of the presentation and go there with start-at-recent-slide, I don't know how to get back to the slide after the one with the question marks once all the examples have been listed. Is there a general way to dynamically generate new slides and then get back to the original structure? Is this sort of thing intended to be a part of slideshow or is this more related to the viewer? Regards, 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.
[racket-users] Re: Legal/Business Case Management DSLs
Hi Richard, My first impulse would be to write the document DSL or DSLs as a Scribble dialect. Scribble allows you to freely insert code in text documents and enables PDF rendering. I'm not sure if there is a best practice for writing Scribble languages, but I've found that it's easier to start from an existing, simple Scribble dialect and add/remove some functionality to get a hang of it. It could also handle the "general Documents language": most Scribble dialects inherit functionality from scribble/base, so there's a parallel. As for the records and reports: if I understand correctly, you don't want separate DSLs for these, but you want to be able to create these from within a "#lang documents/..." file? For instance so that an administrative employee can schedule a meeting directly in the invite, keep contact info in correspondence in sync with records, and so on? I'm pretty sure you can write a Scribble-based language so that you get side effects when you run programs written in it, so executing the document could read/write from/to a database and connect to an email server or web server. I guess you'll still want to review any documents even if the syntax is valid, so posting a preview document to a company-internal web server or sending a preview email, possibly with a link to send out the document definitively and something to roll back/permanently record the changes made to the database are all options. I'm sure others know more how the technical details would work, but it sounds like a fascinating project. I can't commit to anything right now, but it'd be great if you could keep us posted. Regards, 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.
Re: [racket-users] Trying to prove a property of a semantics for logic (Prolog-like) programs: could Redex help?
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 <vince...@gmail.com > > 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 <vince...@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 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?
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 <vince...@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 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?
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.
Re: [racket-users] I've started work on a Racket project book
Thank you, everyone, for the feedback! Comparing even more solutions should be great for learning, so I'll think about an "official" channel for that. Right now, I need some more content first (like the rest of Chapter 1 :-)) but I've opened a ticket so I won't forget. "Emu" is about 40% because the book is about learning by emulating and 60% because it allowed me to use the mascot I have attached here. Regards, Vincent Op zondag 4 juni 2017 13:03:59 UTC+2 schreef Daniel Prager: > Hi Vincent > > Very nice! > > I like the approach of giving exercises along the way, with multiple > solutions to then compare and review against. > > I wonder whether it would be worth having a mechanism whereby readers can > share and discuss their solutions. > > > Also: why "Emu"? > > > Dan -- 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] I've started work on a Racket project book
Hi, I recently read Beautiful Racket and I found it very inspiring, so I started my own Racket project book using Pollen. I'm not a great programmer, but that's the point. Please have a look at it at http://users.telenet.be/vincent-nys/index.html. Feedback is welcome, preferably through https://github.com/v-nys/programming-emu. -- 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] Re: Beautiful Racket v1.0
Congrats! I've gone through all the chapters and it has been the most entertaining programming book I have ever read. It's been practical, too, as I have already used bits of it in a medium-sized (first) Racket project. I would gladly buy it and will recommend it to many of my co-workers. Regards, 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.
