The algebraicity of the lambda-calculus

Abstract. We propose a new definition for abstract syntax (with binding constructions), and, accordingly, for initial semantics and algebraicity. Our definition is based on the notion of module over a monad and its companion notion of linearity. In our setting, we give a one-line definition of an untyped lambda-calculus. Among untyped lambda-calculi, the initial one, the pure untyped lambda-calculus, appears as defined by two algebraic constructions (abs and the unary application app1), together with two algebraic equations which are essentially the β and η rules.

• Type: Journal
• Year: 2007
• Where: CORR
• Authors: André Hirschowitz, Marco Maggesi
• Keywords: Abstract Syntax, CORR 2007, Education, Initial Semantics, Untyped Lambda-calculus