What are “reduction semantics”? Please explain the use of PLT Redex in layman's term

Question

Somebody please explain the usage of reduction semantics and the PLT Redex in simpler language.

Thanks.

Answer 1

Reduction semantics is a computation technique that involves replacing an expression by an equivalent (and hopefully smaller) expression until no more replacement is possible. If a language is Turing-complete, there are expressions that never stop replacing.

Reduction is usually notated by a right arrow, and it's best explained by example:

(3 + 7) + 5   -->  10 + 5  -->  15

This shows the standard reduction semantics for arithmetic expressions. The expression 15 cannot be reduced any further.

Hope this helps.

Answer 2

Reduction semantics are similar (if not the same?) to contextual semantics. Any expression can be broken down into a context and redex.

Robert Harper's Practical Foundations for Programming Languages (draft PDF available here) section 9.3 Contextual Semantics does a decent job of explaining them.

An example:

print 5+4
**context: print [],  redex: 5+4
**evaluate redex: 9
**plug back into context

print 9
**context: [], redex: print 9
**evaluate redex: nil  ==> 9
**plug back into context

nil

You can 'stick' the redex back into the 'hole' of the context to get: print 5+4. The evaluation happens at the redex. You break an expression into a context + redex, evaluate the redex to get a new expression, plug that back into the context, rinse and repeat.

Here's a slightly more complicated example that requires knowledge of an abstract machine that evaluates the lambda calculus:

(lambda x.x+1) 5
**context: [] 5, redex: (lambda x.x+1)
**evaluate redex: <(lambda x.x+1), {environment}> <- create a closure
**plug back into context

<(lambda x.x+1), {}> 5
**context: [], redex: <(lambda x.x+1), {}> 5
**evaluate redex: x+1 where x:=5
**plug back into context

x+1 where x:=5
**context: []+1, redex: x
**evaluate redex: 5 (since x:=5 in our environment)
*plug back into context

5+1...
6

EDIT: The tricky part is recognizing where to break an expression into a context & redex. It requires knowledge of the operational semantics of the language (which 'piece' of an expression you need to evaluate next).