Lambda-Sigma

_Lambda-Sigma_
_lambda-sigma_

This collection provides one file:

 _lambda-sigma.ss_: the lambda-sigma calculus

This library contains a PLT Redex model of the lambda-sigma calculus
of Abadi, Cardelli, Curien, and Lévy.

======================================================================

EXPORTS --------------------------------------------------------------

> λσ : language

The core lambda-sigma language without a definition of evaluation
contexts E.

> λσ/full : language

The lambda-sigma language with evaluation contexts E encoding
arbitrary order, non-deterministic evaluation.

> λσ/normal-order : language

The lambda-sigma language with evaluation contexts E encoding normal
order evaluation.

> (reductions lang) : language -> reduction-relation

Given a lambda-sigma language with a definition of evaluation contexts
E, produces a reduction relation for the lambda-sigma calculus.

> (reduction-graph x) : sexp -> any

Given a lambda-sigma expression, displays a graphical window with
the normal order reduction graph for the expression.

> example1 : sexp

A lambda-sigma representation of (\x.x)(\x.x)

> example2 : sexp

A lambda-sigma representation of ((\x.\y.y)(\x.x))(\x.x)

> example3 : sexp

A lambda-sigma representation of ((\x.\y.xy)(\x.x))(\x.\y.x)

> (whnf? x) : sexp -> boolean

Determines whether a lambda-sigma expression is in weak head normal
form.