# [plt-scheme] Understanding PLT Redex and R6RS Formal Semantics?

 From: Jos Koot (jos.koot at telefonica.net) Date: Thu Feb 19 17:15:20 EST 2009 Previous message: [plt-scheme] Understanding PLT Redex and R6RS Formal Semantics? Next message: [plt-scheme] define-for-meta Messages sorted by: [date] [thread] [subject] [author]

```In the first place see: http://redex.plt-scheme.org/lam-v.html

Redex is a tool that allows:
1: the description of the grammar of a language
2: the description of how an expression of that language is to be reduced to
the value of that expression (reduction relation)
3: after having done steps 1 and 2, redex (in casu procedures traces and
apply-reduction-relation) can show you how an expression is reduced to its
value.

Although Redex is far more general than just a tool to play with Lambda
Calculus (LC) and Combinatory Logic (CL), my path was the following:

0: Imperative programming.
1: The Little LISPer, which is a great primer before glancing into 4. (about
recursion, not really a book about programming, imho)
2: Greg Michaelson, An Introduction to Functional Programming through Lambda
Calculus (not a masterpiece, but easy to read)
3: Playing with Scheme (particularly preparing lots of interpreters.
4: 1984. The Lambda Calculus, Its Syntax and Semantics, Vol. 103 in Studies
in Logic and the Foundations of Mathematics. North-Holland. ISBN
0-444-87508-5. Not easy but very comprehensive.
5: SICP (transformation to continuatian passing style and storage passing
style)
6: Redex, which allows me to check my understanding of LC and CL.

You can regard LC and CL as the ultimate mathematical abstractions of
programming languages. In fact LC consists of the ultimate lambda and
applications only, nothing else. CL goes even further. It has applications
only, no lambda, just a few primitive functions (possibly only one) Yet CL
and LC can be proven to incorporate all "definable functions". These are not
programming languages for practical use, They are formal mathematical
systems of outraging beauty. If you want to make working programs, you'd
better not follow my path, I think.

LC is an important piece of mathematics for the formal study of the
properties of real life programming languages. It is used extensively in
scientific studies on real life programming languages. Scheme can rather
easily be described with mathematical precision in terms of LC. IIRC Algol60
has been described in terms of LC too. As an example, the semantical
description of Scheme-R6RS is based on knowledge based on LC.

Jos

----- Original Message -----
From: "Grant Rettke" <grettke at acm.org>
To: "PLTScheme List" <plt-scheme at list.cs.brown.edu>
Sent: Thursday, February 19, 2009 8:56 PM
Subject: [plt-scheme] Understanding PLT Redex and R6RS Formal Semantics?

> Hi,
>
> I haven't got a clue as to where to even begin understanding what PLT
> Redex solves or how to use it in understanding the R6RS formal
> semantics.
>
> What is this area of study and where does a person start with this stuff?
>
> Best wishes,
>
> Grant
> _________________________________________________