Skip to content

Pattern calculus

Make pattern matching the primitive computational interaction, allowing patterns and pattern abstractions to be constructed, passed, returned, and applied to decompose both functions and data structures.

Version
v2 · 2026-08-30 · History
Domain-specific #
2461
Origin domain
programming language theory
Subdomain
pattern matching calculi and operational semantics

Core Idea

Pattern calculus is a family of formal calculi in which generalized pattern matching, rather than only variable substitution, is the primitive interaction that drives function application and structural decomposition. An application exposes an abstraction's pattern to an argument, a matching operation either produces bindings, detects failure, or waits for more structure, and a successful match substitutes the bindings into the body; because patterns can themselves be represented and transmitted, the calculus supports computation over both functions and structural forms.

Scope of Application

Pattern calculus applies when the analyst can specify a formal term language containing matchable forms, patterns or pattern abstractions, applications, binding positions, and a reduction relation and establish that the formal syntax admits pattern-directed abstractions and the operational semantics reduces their applications through an explicit matching judgment that can inspect constructor structure rather than binding only one undifferentiated variable. The entry is a descriptive account of a formal-computation family. Each theorem, encoding, complexity claim, and programming-language correspondence remains indexed to a named calculus and its published semantics.

Clarity

A clear claim names the carrier, governing rule, assumptions, and recognition test. This matters because pattern calculus can name Barry Jay's broad research program, a particular published calculus, related intensional variants, or the bondi language that demonstrates them. The disciplined statement is that the object counts as Pattern calculus exactly when the formal syntax admits pattern-directed abstractions and the operational semantics reduces their applications through an explicit matching judgment that can inspect constructor structure rather than binding only one undifferentiated variable

Manages Complexity

The abstraction compresses pure and dynamic calculi, intensional and extensional forms, typed and untyped systems, concurrent extensions, constructor-restricted patterns, pattern polymorphism, path polymorphism, and concrete bondi programs into a stable carrier, rule, invariant, and failure boundary. It makes comparison tractable while retaining the variables that control validity.

Abstract Reasoning

  1. Type the carrier. Establish a formal term language containing matchable forms, patterns or pattern abstractions, applications, binding positions, and a reduction relation and reject examples from a different problem. 2. Lock the rule. Express that the formal syntax admits pattern-directed abstractions and the operational semantics reduces their applications through an explicit matching judgment that can inspect constructor structure rather than binding only one undifferentiated variable independently of one notation or implementation.

Knowledge Transfer

Transfer within programming language theory is strong when new cases preserve the same carrier, mechanism, and diagnostic. The move from In a pure pattern calculus, an abstraction pairs a pattern with a body, and applying it to a matchable term first computes a match before substituting the resulting bindings into the body. to The bondi research language used pattern abstractions to express generic eliminators and queries that traverse structurally different values without writing one eliminator per constructor family. demonstrates that continuity.

Relationships to Other Abstractions

Local relationship map for Pattern calculusParents appear above the current abstraction, mutual partners to the right, and children below. Node labels state whether each abstraction is prime or domain-specific; colors identify relation types.Pattern calculusDOMAINPrime abstraction: Higher Order Function — is a kind ofHigher OrderFunctionPRIME

Current abstraction Pattern calculus Domain-specific

Parents (1) — more general patterns this builds on

  • Pattern calculus is a kind of Higher Order Function Prime

    The proposed strict upward parent is prime:higher_order_function.

Hierarchy path (1) — routes to 1 parentless root

Neighborhood in Abstraction Space

Pattern calculus sits in a moderately populated region (42nd percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.

Family — Syntax, Rewriting & Declarative Form (41 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-09-08