Recursive programs in normal form (short paper)

© 2018 Association for Computing Machinery. Recursive programs can now be expressed as normal forms within some rewriting systems, including traditional combinatory logic, a new variant of lambda-calculus called closure calculus, and recent variants of combinatory logic that support queries of internal program structure. In all these settings, partial evaluation of primitive recursive functions, such as addition, can reduce open terms to normal form without fear of non-termination. In those calculi where queries of program structure are supported, program optimisations that are expressed as non-standard rewriting rules can be represented as functions in the calculus, without any need for quotation or other meta-theory