Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Functional Machine Calculus III: Choice (Early Announcement)

Willem Heijltjes

Abstract

The Functional Machine Calculus (Heijltjes 2022) is an extension of the lambda-calculus that preserves confluent reduction and typed termination, while enabling both call-by-name and call-by-value reduction behaviour and encoding the computational effects of mutable higher-order store, input/output, and probabilistic computation. In this note the calculus is extended to capture exception handling and loop constructs.

The Functional Machine Calculus III: Choice (Early Announcement)

Abstract

The Functional Machine Calculus (Heijltjes 2022) is an extension of the lambda-calculus that preserves confluent reduction and typed termination, while enabling both call-by-name and call-by-value reduction behaviour and encoding the computational effects of mutable higher-order store, input/output, and probabilistic computation. In this note the calculus is extended to capture exception handling and loop constructs.

Paper Structure

This paper contains 7 sections, 4 theorems, 26 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Background
  3. Development
  4. The FMC with Choice
  5. Types
  6. Discussion
  7. Conclusion

Key Result

Proposition 4.3

The normal forms ${ \newline( \color{term} N \color{black} \color{black} 0\@end }$ of reduction $\mathrel{\begin{tikzpicture}\draw[rw] (0,0)--(10pt,0pt);\end{tikzpicture}}$ are given by the following grammars.

Figures (1)

  • Figure 1: Typing rules

Theorems & Definitions (13)

  • Definition 4.1
  • Definition 4.2
  • Proposition 4.3
  • Definition 4.4
  • Definition 4.5
  • Proposition 4.6
  • Proposition 4.7
  • Conjecture 4.8
  • Definition 5.1
  • Definition 5.2
  • ...and 3 more