[plt-scheme] (Off) Tool for Visualizing Beta-Reductions?

From: Carl Eastlund (cce at ccs.neu.edu)
Date: Thu Aug 7 09:05:22 EDT 2008

On Thu, Aug 7, 2008 at 8:08 AM, Erich Rast <erich at snafu.de> wrote:
> Hi,
> Sorry for this slightly off-topic question. I'm working in intensional
> natural language semantics (aka "Montague Grammar"), where the lexical
> meaning of expressions is sometimes (not always) specified in ordinary
> language, like in this example where the expression type is given as a
> subscript:
> (\lambda x_e. x_e walks) john_e
> ==> john_e walks
> Now imagine rather complicated formulas with complex functional types
> and lots of function applications. Think of generalized quantifiers
> being modified by prepositions to yield sentence- to sentence-type
> operators and fancy stuff like that. It turns out to be very cumbersome
> and error-prone to do all the beta-reductions by hand that come up in
> examples.
> Does anyone know a tool that visualizes individual reduction steps, but
> also allows for the inclusion of arbitrary strings like "walks" in the
> above trivial example? Can the PLT redex tool be used for this?
> Best regards,
> Erich

PLT Redex can do a lot of that.  Certainly, it doesn't check
automatically whether variables are bound, so "walks" won't pose a
problem.  It uses "_" in its own naming convention, though, so you'd
have to fit your variable-typing convention into PLT Redex's
convention, and recognize typed identifiers yourself or give them a
compound form (e.g. "(typed john e)").  Other than that, sounds like
PLT Redex is exactly what you want.

Carl Eastlund

Posted on the users mailing list.