Beyond Lambda-Calculus: Intensional Computation

A SkillsCast for this session is not available.

There is a paradox in the foundations of computing. On the one hand, lambda calculus is supposed to compute anything that can be computed. On the other hand, many intensional computations, such as deciding equality of programs (terms in closed normal form), are not definable within lambda calculus. The paradox has now been resolved by close reading of the original papers and books, which clarifies that lambda calculus is inherently extensional.

More importantly, there are new, intensional calculi which are more expressive than lambda calculus. First, pattern calculus supports both higher-order functions and generic queries of data structures, by basing all computation on pattern matching. Second, SF-calculus can query programs as well as data structures by factoring them, using the operator F. In particular, the Goedel number of a program can be defined within the calculus itself.Third, lambda-SF calculus adds native support for lambda-abstraction to SF-calculus. Other calculi are currently under development.

Pattern calculus has been realised in the programming language, bondi. Even better programming languages are now possible.

YOU MAY ALSO LIKE:

• Making Less of the Web with Feature Policy (SkillsCast recorded in July 2019)
• Experimenting with Distributed Data Processing in Haskell (SkillsCast recorded in May 2019)