|
Sébastien Carlier and J. B. Wells
The
algebra of expansion
Draft corresponding roughly to an ITRS 2008 workshop talk, March 2008
Expansion is an operation on typings (pairs of type
environments and result types) in type systems for
the lambda-calculus. Expansion was originally
introduced for calculating possible typings of a
term in systems with intersection types.
Unfortunately, definitions of expansion (even the
most modern ones) have been difficult for outsiders
to absorb. This paper aims to clarify expansion and
make it more accessible to non-specialists by
isolating the pure notion of expansion on its own,
independent of type systems and types. We show how
expansion can be seen as a simple algebra on terms
with variables, substitutions, composition, and
miscellaneous constructors such that the algebra
satisfies 8 simple axioms and axiom schemas: the 3
standard axioms of a monoid, 4 standard axioms or
axiom schemas of substitutions (including one that
corresponds to the usual “substitution lemma''),
and 1 axiom schema for expansion itself. This
presentation should help make more accessible to a
wider community theory and techniques involving
intersection types and type inference with flexible
precision.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
|
