2025/10/09 by Willem Heijltjes, Heijltjes, Willem
Computer Science · Engineering · #Advanced Control Systems Optimization #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Fuzzy Logic and Control Systems #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2510.07851
openalex publication_date 2025/10/09 · openalex created_date 2025/10/18 · openalex updated_date 2026/08/03
The Functional Machine Calculus (Heijltjes 2022) is a new approach to unifying the imperative and functional programming paradigms. It extends the lambda-calculus, preserving the key features of confluent reduction and typed termination, to embed computational effects, evaluation strategies, and control flow operations. The first instalment modelled sequential higher-order computation with global store, input/output, probabilities, and non-determinism, and embedded both the call-by-name and call-by-value lambda-calculus, as well as Moggi's computational metalanguage and Levy's call-by-push-value. The present paper extends the calculus from sequential to branching and looping control flow. This allows the faithful embedding of a minimal but complete imperative language, including conditionals, exception handling, and iteration, as well as constants and algebraic data types. The calculus is defined through a simple operational semantics, extending the (simplified) Krivine machine for the lambda-calculus with multiple operand stacks to model effects and a continuation stack to model sequential, branching, and looping computation. It features a confluent reduction relation and a system of simple types that guarantees termination of the machine and strong normalization of reduction (in the absence of iteration). These properties carry over to the embedded imperative language, providing a unified functional-imperative model of computation that supports simple types, a direct and intuitive operational semantics, and a confluent reduction semantics.