Choice Calculus
The choice calculus is a simple, formal language for representing variation.
This research was originally motivated by improving the development and maintenance of massively configurable software, such as software product lines. However, it has since been applied to modeling software resource consumption, optimizing gradually typed programs, typing generalized algebraic data types, improving error location during type inference, and more.
The core choice calculus is very small—just two constructs, choices and generic object language abstract syntax tree nodes—but can be extended with additional language features that support different ways of representing and computing with variability. The language is generic, emphasizing that variation can often be treated orthogonally to other concerns, but it can be instantiated by different object languages and data types when they interact fundamentally with variability.
The primary reference for the choice calculus is the original TOSEM paper [3], while the most comprehensive introduction is my PhD dissertation [1]. The tutorial from the 2011 GTTSE Summer School [2] is also a good (and hopefully fun) entry point. The tutorial promotes the idea of “variation anywhere” and of generically lifting non-variational algorithms to variational ones.
However, these early works present a slightly more complex version of the calculus than we typically use now. For example, see Section 2 of FOSD’16 [5] for a much simpler and more concise introduction.
Introductions to the Choice Calculus
- The Choice Calculus: A Formal Language of Variation[Abstract, PDF]PhD dissertation, Oregon State University, 2013
In this thesis I present the choice calculus, a formal language for representing variation in software and other structured artifacts. The choice calculus is intended to support variation research in a way similar to the lambda calculus in programming language research. Specifically, it provides a simple formal basis for presenting, proving, and communicating theoretical results. It can serve as a common language of discourse for researchers working on different views of similar problems and provide a shared back end in tools.
This thesis collects a large amount of work on the choice calculus. It defines the syntax and denotational semantics of the language along with modular language extensions that add features important to variation research. It presents several theoretical results related to the choice calculus, such as an equivalence relation that supports semantics-preserving transformations of choice calculus expressions, and a type system for ensuring that an expression is well formed. It also presents a Haskell DSEL based on the choice calculus for exploring the concept of variational programming.
- Variation Programming with the Choice Calculus[Abstract, PDF, Code]Generative and Transformational Techniques in Software Engineering IV (GTTSE 2011), Revised and Extended Papers, LNCS vol. 7680, Springer, 2013, 55–100
The choice calculus provides a language for representing and transforming variation in software and other structured documents. Variability is captured in localized choices between alternatives. The space of all variations is organized by dimensions, which provide scoping and structure to choices. The variation space can be reduced through a process of selection, which eliminates a dimension and resolves all of its associated choices by replacing each with one of their alternatives. The choice calculus also allows the definition of arbitrary functions for the flexible construction and transformation of all kinds of variation structures. In this tutorial we will first present the motivation, general ideas, and principles that underlie the choice calculus. This is followed by a closer look at the semantics. We will then present practical applications based on several small example scenarios and consider the concepts of “variation programming” and “variation querying”. The practical applications involve work with a Haskell library that supports variation programming and experimentation with the choice calculus.
- The Choice Calculus: A Representation for Software Variation[Abstract, PDF]ACM Trans. on Software Engineering and Methodology (TOSEM), vol. 21, num. 1, 2011, 6:1–6:27
Many areas of computer science are concerned with some form of variation in software–from managing changes to software over time, to supporting families of related artifacts. We present the choice calculus, a fundamental representation for software variation that can serve as a common language of discourse for variation research, filling a role similar to the lambda calculus in programming language research. We also develop an associated theory of software variation, including sound transformations of variation artifacts, the definition of strategic normal forms, and a design theory for variation structures, which will support the development of better algorithms and tools.
Extensions of the Choice Calculus
- A Calculus for Variational Programming[Abstract, PDF]European Conf. on Object-Oriented Programming (ECOOP), LIPIcs vol. 56, 2016, 6:1–6:28
Variation is ubiquitous in software. Many applications can benefit from making this variation explicit, then manipulating and computing with it directly—a technique we call “variational programming”. This idea has been independently discovered in several application domains, such as efficiently analyzing and verifying software product lines, combining bounded and symbolic model-checking, and computing with alternative privacy profiles. Although these domains share similar core problems, and there are also many similarities in the solutions, there is no dedicated programming language support for variational programming. This makes the various implementations tedious, prone to errors, hard to maintain and reuse, and difficult to compare.
In this paper we present a calculus that forms the basis of a programming language with explicit support for representing, manipulating, and computing with variation in programs and data. We illustrate how such a language can simplify the implementation of variational programming tasks. We present the syntax and semantics of the core calculus, a sound type system, and a type inference algorithm that produces principal types.
- Formula Choice Calculus[Abstract, PDF, Code]Int. Workshop on Feature-Oriented Software Development (FOSD), ACM, 2016, 49–57
The choice calculus is a simple metalanguage and associated theory that has been successfully applied to several problems of interest to the feature-oriented software development community. The formal presentation of the choice calculus essentially restricts variation points, called choices, to vary based on the inclusion or not of a single feature, while in practice variation points may depend on several features. Therefore, in both theoretical applications of the choice calculus, and in tools inspired by the choice calculus, the syntax of choices has often been generalized to depend on an arbitrary propositional formula of features. The purpose of this paper is to put this syntactic generalization on more solid footing by also generalizing the associated theory. Specifically, after defining the syntax and denotational semantics of the formula choice calculus (FCC), we define and prove the soundness of a syntactic equivalence relation on FCC expressions. This effort validates previous work which has implicitly assumed the soundness of rules in the equivalence relation, and also reveals several rules that are specific to FCC. Finally, we describe some further generalizations to FCC and their limits.
- Adding Configuration to the Choice Calculus[Abstract, PDF]Int. Workshop on Variability Modelling of Software-Intensive Systems (VaMoS), ACM, 2013, 13:1–13:8
The choice calculus is a formal language for representing variation in software artifacts. Variability is organized in the choice calculus through the use of dimensions, where each dimension represents a decision that must be made in order to obtain a particular variant. However, the process of selecting alternatives from dimensions was relegated to an external operation. This precludes many interesting variation and reuse patterns, such as nested product lines, and theoretical results, such as a syntactic description of configuration, that would be possible if selection were a part of the language itself.
In this paper we add a selection operation to the choice calculus and illustrate how that increases the expressiveness of the calculus. We investigate some alternative semantics of this operation and study their impact and utility. Specifically, we will examine selection in the context of static and dynamically scoped dimension declarations, as a well as a modest and greedy form of dimension elimination. We also present a design for a type system to ensure configuration safety and modularity of nested product lines.
- A Calculus for Modeling and Implementing Variation[Abstract, PDF]ACM SIGPLAN Int. Conf. on Generative Programming and Component Engineering (GPCE), 2012, 132–140
We present a formal calculus for modeling and implementing variation in software. It unifies the compositional and annotative approaches to feature implementation and supports the development of abstractions that can be used to directly relate feature models to their implementation. Since the compositional and annotative approaches are complementary, the calculus enables implementers to use the best combination of tools for the job and focus on inherent feature interactions, rather than those introduced by biases in the representation. The calculus also supports the abstraction of recurring variational patterns and provides a metaprogramming platform for organizing variation in artifacts.
Related Projects
The choice calculus is at the heart of several of my other research projects, including:
Variational Programming
Efficiently computing with massive variation in data and code.Variational Typing
Efficiently inferring types for variational programs.Variation Control Systems
Editing and managing variational software.