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

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