[plt-scheme] How to learn about typical applications of the match library?

On 12/07/07, Grant Rettke <grettke at acm.org> wrote:
> What are some examples of that which against you are matching?
>

Formulas written as lists like
'(<=> (=> a b) c)

But with thousands of variables and operators, generated automatically.

Cheers,

Paulo Matos

> On 7/11/07, Paulo J. Matos <pocm at soton.ac.uk> wrote:
> > On 10/07/07, Grant Rettke <grettke at acm.org> wrote:
> > > Lately I've seen examples of match, match-let is one thing that
> > > immediately makes sense.
> > >
> > > What are some other typical applications of let? Where are some places
> > > to read up on it?
> >
> > I use PLT-match _a lot_.
> > Here's an example from my own work (soon in a planet near you)
> > Which converts some fol formulas into formulas with only ands ors and nots.
> > (define (remove-redundant-ops f)
> >     (match f
> >       (`(=> ,op1 ,op2)
> >         `(or (not ,(remove-redundant-ops op1))
> >              ,(remove-redundant-ops op2)))
> >       (`(<=> ,op1 ,op2)
> >         (remove-redundant-ops
> >          `(and (=> ,op1 ,op2)
> >                (=> ,op2 ,op1))))
> >       (`(xor ,op1 ,op2)            ;; Binary xor
> >         (remove-redundant-ops
> >          `(not (<=> ,op1 ,op2))))
> >       (`(ite ,op1 ,op2 ,op3)
> >         (remove-redundant-ops
> >          `(and (=> ,op1 ,op2)
> >                (=> (not ,op1) ,op3))))
> >       (`(xor ,ops ..3)            ;; Multiple argument xor, which is
> > true iff exactly only one of the ops is true
> >        (remove-redundant-ops
> >         `(and (or , at ops)
> >               ,(apply encode-atmost1 ops))))
> >       (`(am1 ,ops ..2)            ;; Multiple argument atmost1
> > operator, encoding of cardinality constraints used
> >        (remove-redundant-ops (apply encode-atmost1 ops)))
> >       (`(and ,ops ..1)
> >         `(and ,@(map remove-redundant-ops ops)))
> >       (`(or ,ops ..1)
> >         `(or ,@(map remove-redundant-ops ops)))
> >       (`(not ,op)
> >         `(not ,(remove-redundant-ops op)))
> >       ((? symbol? s) s)
> >       (_ (error 'remove-redundant-ops "Couldn't find a match for ~a" f))))
> >
> >
> > The encode-atmost1 is the encoding for the cardinality constraint
> > AtMost presented in Carsten Sinz paper on CP2005.
> >
> > And my PLTScheme model checker for formal specifications include
> > _lots_ of applications of plt-scheme besides this one.
> >
> > Cheers,
> >
> > Paulo Matos
> >
> > > _________________________________________________
> > >   For list-related administrative tasks:
> > >   http://list.cs.brown.edu/mailman/listinfo/plt-scheme
> > >
> > >
> > >
> >
> >
> > --
> > Paulo Jorge Matos - pocm at soton.ac.uk
> > http://www.personal.soton.ac.uk/pocm
> > PhD Student @ ECS
> > University of Southampton, UK
> >
>
>
>


-- 
Paulo Jorge Matos - pocm at soton.ac.uk
http://www.personal.soton.ac.uk/pocm
PhD Student @ ECS
University of Southampton, UK