Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus

Naoki Kobayashi

TL;DR

The paper analyzes the reachability problem in extensions of the simply typed lambda calculus (finitary PCF). It proves undecidability for four side-effect extensions (exceptions, algebraic effects with handlers, symbol generation, and Boolean references) by encoding Minsky machines, illustrating the source of undecidability. It then introduces a decidable fragment, PCF^{ref, lin}_{eta}, that restricts closures to linear ownership of references and provides a type-based translation to pure PCF, establishing decidability for the Boolean base and enabling automated verification via existing higher-order model-checkers. The work further discusses extensions (fractional ownerships, borrowing, product/sum types, higher-order references) and reports preliminary experiments translating OCaml-like programs, highlighting practical applications to verification tools like MoCHi. Overall, the results inform language design and verification tooling by balancing expressiveness with decidability through ownership-conscious type systems.

Abstract

The decidability of the reachability problem for finitary PCF has been used as a theoretical basis for fully automated verification tools for functional programs. The reachability problem, however, often becomes undecidable for a slight extension of finitary PCF with side effects, such as exceptions, algebraic effects, and references, which hindered the extension of the above verification tools for supporting functional programs with side effects. In this paper, we first give simple proofs of the undecidability of four extensions of finitary PCF, which would help us understand and analyze the source of undecidability. We then focus on an extension with references, and give a decidable fragment using a type system. To our knowledge, this is the first non-trivial decidable fragment that features higher-order recursive functions containing reference cells.

On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus

TL;DR

The paper analyzes the reachability problem in extensions of the simply typed lambda calculus (finitary PCF). It proves undecidability for four side-effect extensions (exceptions, algebraic effects with handlers, symbol generation, and Boolean references) by encoding Minsky machines, illustrating the source of undecidability. It then introduces a decidable fragment, PCF^{ref, lin}_{eta}, that restricts closures to linear ownership of references and provides a type-based translation to pure PCF, establishing decidability for the Boolean base and enabling automated verification via existing higher-order model-checkers. The work further discusses extensions (fractional ownerships, borrowing, product/sum types, higher-order references) and reports preliminary experiments translating OCaml-like programs, highlighting practical applications to verification tools like MoCHi. Overall, the results inform language design and verification tooling by balancing expressiveness with decidability through ownership-conscious type systems.

Abstract

The decidability of the reachability problem for finitary PCF has been used as a theoretical basis for fully automated verification tools for functional programs. The reachability problem, however, often becomes undecidable for a slight extension of finitary PCF with side effects, such as exceptions, algebraic effects, and references, which hindered the extension of the above verification tools for supporting functional programs with side effects. In this paper, we first give simple proofs of the undecidability of four extensions of finitary PCF, which would help us understand and analyze the source of undecidability. We then focus on an extension with references, and give a decidable fragment using a type system. To our knowledge, this is the first non-trivial decidable fragment that features higher-order recursive functions containing reference cells.

Paper Structure

This paper contains 27 sections, 16 theorems, 76 equations, 10 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Boolean PCF (BPCF)
  4. Minsky Machines
  5. Undecidable Extensions of Boolean PCF
  6. Boolean PCF with Exceptions (BPCF$^{\mathit{exn}}$)
  7. An Extension with Algebraic Effects and Handlers (BPCF$^{\mathit{alg}}$)
  8. Encoding of Minsky machines with shallow handlers
  9. Encoding of Minsky machines with deep handlers
  10. Extension with Symbol Generation
  11. Extension with Boolean References
  12. Decidable References
  13. Overview
  14. Syntax and Type System of PCF$^{\mathit{ref, lin}}_{\mathbf{b}}$
  15. Translation from PCF$^{\mathit{ref, lin}}_{\mathbf{b}}$ to PCF$_{\mathbf{b}}$
  16. ...and 12 more sections

Key Result

Theorem 3.1

The reachability problem for Boolean PCF with exceptions, i.e., the problem of deciding whether $M\longrightarrow^*\mathtt{fail}$ is undecidable.

Figures (10)

  • Figure 1: Typing Rules for Boolean PCF
  • Figure 2: Reduction Semantics
  • Figure 3: Typing Rules for Algebraic Effects
  • Figure 4: Operational Semantics for Algebraic Effects. The meta-variable $F$ denotes an evaluation context without a sub-expression of the form $\mathtt{with}\; H\;\mathtt{handle}\;E$ and $F$ does not capture $y$.
  • Figure 5: Typing Rules for PCF$^{\mathit{ref, lin}}_{\mathbf{b}}$
  • ...and 5 more figures

Theorems & Definitions (45)

  • Definition 2.1: reachability problem
  • Remark 2.1
  • Remark 2.2
  • Definition 2.2: Minsky machine
  • Definition 2.3: Minsky machine halting problem
  • Theorem 3.1: DBLP:journals/lisp/Lillibridge99
  • Remark 3.1
  • Remark 3.2
  • Remark 3.3
  • Theorem 3.2
  • ...and 35 more