Name
Abstract | ||
|---|---|---|
We formalize a technique introduced by Böhm and Piperno to solve systems of recursive equations in lambda calculus without the use of the fixed point combinator and using only normal forms. To this aim we introduce the notion of a canonical algebraic term rewriting system, and we show that any such system can be interpreted in the lambda calculus by the Böhm — Piperno technique in such a way that strong normalization is preserved. This allows us to improve some recent results of Mogensen concerning efficient gödelizations : of lambda calculus. In particular we prove that under a suitable gödelization there exist two lambda terms E (self-interpreter) and R (reductor), both having a normal form, such that for every (closed or open) lambda term M EMM and if M has a normal form N, then RMN. |
Year | Venue | Keywords |
|---|---|---|
1992 | Lecture Notes in Computer Science | normal form,lambda calculus |
Field | DocType | ISBN |
Deductive lambda calculus,Discrete mathematics,Typed lambda calculus,Simply typed lambda calculus,Fixed-point combinator,System F,Church encoding,Lambda lifting,Pure type system,Mathematics | Conference | 3-540-56992-8 |
Citations | PageRank | References |
11 | 0.81 | 5 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alessandro Berarducci | 1 | 136 | 22.96 |
| Corrado Böhm | 2 | 487 | 413.44 |