Intensional computation with higher-order functions

© 2019 Elsevier B.V. Intensional computations are those that query the internal structure of their arguments. In a higher-order setting, such queries perform program analysis. This is beyond the expressive power of traditional term rewriting systems, such as lambda-calculus or combinatory logic, as they are extensional. In such settings it has been necessary to encode or quote the program before analysis. However, there are intensional calculi, specifically confluent term rewriting systems, that can analyse higher-order programs within the calculus proper, without quotation; there are even programs that produce the Goedel numbers of their program argument. This paper summarizes the current situation. Highlights include the following observations. We have known since 2011 that the simplest intensional calculus, SF-calculus, supports arbitrary queries of closed normal forms, including equality, pattern-matching, searching and self-interpretation. Recent work, verified using the Coq proof assistant, has shown that all recursive programs can be represented as closed normal forms in SF-calculus, and even in combinatory logic. Thus, we can here deduce that SF-calculus (but not combinatory logic) can define queries of programs. These results are compatible with direct support for lambda-abstraction. Although these results conflict with the traditional understanding of expressive power of combinatory logic and λ-calculus, as developed by Church and Kleene, our recent publication has shown that their approach is compromised by its reliance on encodings. To drive the point home, this paper uses a non-standard encoding to lambda-define a trivial solution of the Halting Problem