λvc:   Variadic Auto-Curried Lambda Calculus
1 Background
2 Using the Reference Interpreter
3 Syntax
4 Semantics
7.9

λvc: Variadic Auto-Curried Lambda Calculus

Pierce Darragh <pierce.darragh@gmail.com>

This package implements λvc: the lambda calculus extended to support variadic functions and automatic currying of multary functions. The code lives on GitHub at pdarragh/variadic-curry-calculus.

    1 Background

    2 Using the Reference Interpreter

    3 Syntax

    4 Semantics

1 Background

On November 18, 2020, Twitter user @fogus sent out a tweet asking:

If you had a Lisp with auto-currying what would you expect as the application of ((- 1) 2)?

Traditionally, the Lisp arithmetic functions are variadic. This means they can be given any number of arguments and compute a result:

> (+ 1)
1
> (+ 1 2)
3
> (+ 1 2 3)
6

Meanwhile, auto-currying refers to a language feature where functions that accept multiple arguments are converted into sets of nested functions that each accept only one argument, with the intermediate functions returning functions themselves. In a Lisp-like lambda calculus notation, this might look like:

;; We put in a function that takes three arguments...
> (λ (x1 x2 x3) t)
;; And we get back a nesting of three single-argument functions.
(λ (x1) (λ (x2) (λ (x3) t)))

This means that, in a sane programming language, variadic functions and auto-currying are at odds. A variadic functions says "I take any number of arguments in my last parameter" while automatic currying says "Functions may only take one argument at a time." When you apply a variadic function to more than one value in a language with automatic currying, a question is raised: is the second value an additional variadic argument, or is it meant to be used in the application of the result of the first application?

To resolve this truly nefarious problem, λvc implements what I call superpositions, a term borrowed from quantum physics. In physics, the superposition is the notion that a system may exist in multiple distinct states simultaneously until it is observed. Generally, the states each have a distinct probability, and this probability plays a role in determining which state will remain when the system is observed.

In λvc, the superposition encodes two statesEither of those states can itself be a superposition, so representing a superposition of more than two states is possible by nesting. that are considered "equally likely" (in that no probability is assigned). Observation occurs through application. When a superposition is applied to a value, application distributes across both branches of the superposition: the result of the variadic function that begat the superposition as well as the variadic function itself as though it were waiting for an additional argument.

To make this work, variadic functions must be declared within the context of another non-nullary function. When a variadic function is applied, we evaluate its body with the proper substitution as though it were a regular unary function. However, we also construct a new version of the variadic function with an updated environment. In this environment, the value bound during application of the parent function is replaced with the result of the variadic application. This is kept around in the variadic closure for subsequent applications (if any).

2 Using the Reference Interpreter

This package provides a reference interpreter for λvc. After installing this package, you can (require lambda-vc). Only one function is exposed: interp. The recommended way to interact with this function is through quotation:

> (require lambda-vc)
> (interp `((λ (x) x) 42))
42

The reference interpreter will accept lambda in place of λ. The exposed interp function operates in a big-step style, meaning it eagerly evaluates results until it gets either a value or an error. There may come a day when I change the exposed API to provide both small- and big-step interpreters, but today is not that day.

In addition, the reference interpreter provides a few arithmetic functions that can be used: +, -, *, and /. Using these, let’s explore variadic functions:

;; First, let's see what happens when we interpret a variadic function.
> (interp `(λ (a b ...) (+ a b)))
(λ (a) (λ (b ...) (+ a b)))
;; Now, let's apply it to a value.
> (interp `((λ (a b ...) (+ a b)) 1))
(λ (b ...) (+ a b))
;; λvc does not substitute eagerly, so this is correct.
;; Now, let's apply a second value.
> (interp `((λ (a b ...) (+ a b)) 1 2))
(σ 3 (λ (b ...) (+ a b)))
;; We can apply the result a few more times...
> (interp `((λ (a b ...) (+ a b)) 1 2 3 4 5))
(σ 15 (λ (b ...) (+ a b)))

Each time we apply the variadic function, the resulting value is substituted in for the a that was previously bound to the preceding value. As a result, we get a superposition which represents the fact that we don’t know whether we are done applying the function or if it should continue to accept additional arguments.

3 Syntax

This section defines the valid syntax that can be used in constructing terms in λvc. A superscript * indicates a repetition of the preceding item zero or more times. The superscript + indicates a repetition of the preceding item one or more times. The lambda λ, sigma σ, ellipsis ..., and parentheses () are all literals.

t ::=

 

 

terms:

 

z

 

 

integer

 

x

 

 

variable

 

(λ (x*) t)

 

 

n-ary function

 

(λ (x+ ...) t)

 

 

variadic function

 

(σ t t)

 

 

superposition

 

(t+)

 

 

application

 

 

 

v ::=

 

 

values:

 

z

 

 

integer value

 

(λ () t)

 

 

nullary function value

 

(λ (x) t)

 

 

unary function value

 

(λ (x ...) t)

 

 

variadic function value

 

(σ v v)

 

 

superposition value

4 Semantics

These are the operational semantics of λvc. The \longrightarrow indicates an evaluation that can be taken in a single step. The \longrightarrow^{\ast} indicates an evaluation whose result can be reached in zero or more steps. (I have tried to reduce the use of \longrightarrow^{\ast} as much as possible to provide a small-step semantics, but this was tricky for variadic functions.)

The \epsilon indicates an error value. Although I did not specifically label them, any invalid evaluation step will produce an error value \epsilon. In almost all cases, these will short-circuit the reference interpreter to be returned to the user. The notable exception to this behavior is when an error value is obtained as the result of evaluating one arm of a superposition, in which case the superposition collapses and only the other arm remains. (If both arms produce errors, then an error is returned.)

\lambda, \sigma, \ldots, and \left(\right) are syntactic literals. \mathtt{\mathbf{t}} represents terms, \mathtt{\mathbf{x}} represents variables, and \mathtt{\mathbf{v}} represents values, as per the definitions given in the preceding section. Subscripts are used on \mathtt{\mathbf{t}}, \mathtt{\mathbf{x}}, and \mathtt{\mathbf{v}} to disambiguate specific instances, and these subscripts are numbered from left to right in order of appearance in the conclusion of each judgment rule as a convention.

{\rm E}\text{-}{\rm S {\small UBSTITUTE}}

 

{} \over {\Gamma\left[{\mathtt{\mathbf{x}}}_{1} \mapsto {\mathtt{\mathbf{v}}}_{2}\right]{\ }\vdash{\ } {\mathtt{\mathbf{x}}}_{1} {\ }\longrightarrow{\ } \Gamma{\ }\vdash{\ } {\mathtt{\mathbf{v}}}_{2}}

{\rm E}\text{-}{\rm C {\small URRY}}

 

{} \over {\left(\lambda {\ } \left({\mathtt{\mathbf{x}}}_{1} {\ } {\mathtt{\mathbf{x}}}_{2}^{+} \right) {\ } {\mathtt{\mathbf{t}}}_{3}\right) {\ }\longrightarrow{\ } \left(\lambda {\ } \left({\mathtt{\mathbf{x}}}_{1} \right) {\ } \left(\lambda {\ } \left({\mathtt{\mathbf{x}}}_{2}^{+} \right) {\ } {\mathtt{\mathbf{t}}}_{3}\right)\right)}

{\rm E}\text{-}{\rm A {\small PP} U {\small NCURRY}}

 

{} \over {\left({\mathtt{\mathbf{t}}}_{1} {\ } {\mathtt{\mathbf{t}}}_{2} {\ } {\mathtt{\mathbf{t}}}_{3} ^{+}\right) {\ }\longrightarrow{\ } \left(\left({\mathtt{\mathbf{t}}}_{1} {\ } {\mathtt{\mathbf{t}}}_{2}\right) {\ } {\mathtt{\mathbf{t}}}_{3} ^{+}\right)}

{\rm E}\text{-}{\rm A {\small PP} R {\small EDUCE} 1}

 

{{{{\mathtt{\mathbf{t}}}_{1} {\ }\longrightarrow{\ } {\mathtt{\mathbf{t}}}_{1} ’}}} \over {{\left({\mathtt{\mathbf{t}}}_{1} {\ } {\mathtt{\mathbf{t}}}_{2}\right) {\ }\longrightarrow{\ } \left({\mathtt{\mathbf{t}}}_{1} ’ {\ } {\mathtt{\mathbf{t}}}_{2}\right)}}

{\rm E}\text{-}{\rm A {\small PP} R {\small EDUCE} 2}

 

{{{{\mathtt{\mathbf{t}}}_{2} {\ }\longrightarrow{\ } {\mathtt{\mathbf{t}}}_{2} ’}}} \over {{\left({\mathtt{\mathbf{v}}}_{1} {\ } {\mathtt{\mathbf{t}}}_{2}\right) {\ }\longrightarrow{\ } \left({\mathtt{\mathbf{v}}}_{1} {\ } {\mathtt{\mathbf{t}}}_{2} ’\right)}}

{\rm E}\text{-}{\rm A {\small PP} R {\small EDUCE} 3}

 

{} \over {{\left({\mathtt{\mathbf{v}}}_{1} {\ } \left(\sigma {\ } {\mathtt{\mathbf{v}}}_{2} {\ } {\mathtt{\mathbf{v}}}_{3}\right)\right) {\ }\longrightarrow{\ } \left(\sigma {\ } \left({\mathtt{\mathbf{v}}}_{1} {\ } {\mathtt{\mathbf{v}}}_{2}\right) {\ } \left({\mathtt{\mathbf{v}}}_{1} {\ } {\mathtt{\mathbf{v}}}_{3}\right)\right)}}

{\rm E}\text{-}{\rm A {\small PP} N {\small ULL}}

 

{{{{\mathtt{\mathbf{t}}}_{1} {\ }\longrightarrow{\ } {\mathtt{\mathbf{t}}}_{1} ’}}} \over {{\left(\left(\lambda {\ } \left({\ } \right) {\ } {\mathtt{\mathbf{t}}}_{1}\right)\right) {\ }\longrightarrow{\ } {\mathtt{\mathbf{t}}}_{1} ’}}

{\rm E}\text{-}{\rm A {\small PP} U {\small NARY}}

 

{} \over {\left(\left(\lambda {\ } \left({\mathtt{\mathbf{x}}}_{1} \right) {\ } {\mathtt{\mathbf{t}}}_{2}\right) {\ } {\mathtt{\mathbf{v}}}_{3}\right) {\ }\longrightarrow{\ } \Gamma\left[{\mathtt{\mathbf{x}}}_{1} \mapsto {\mathtt{\mathbf{v}}}_{3}\right]{\ }\vdash{\ } {\mathtt{\mathbf{t}}}_{2}}

{\rm E}\text{-}{\rm A {\small PP} V {\small ARIADIC}}

 

{{{\Gamma\left[{\mathtt{\mathbf{x}}}_{1} \mapsto {\mathtt{\mathbf{v}}}_{2},{\ } {\mathtt{\mathbf{x}}}_{3} \mapsto {\mathtt{\mathbf{v}}}_{5}\right]{\ }\vdash{\ } {\mathtt{\mathbf{t}}}_{4} {\ }\longrightarrow^{\ast}{\ } {\mathtt{\mathbf{v}}}_{6}}}} \over {{\small \Gamma\left[{\mathtt{\mathbf{x}}}_{1} \mapsto {\mathtt{\mathbf{v}}}_{2}\right]{\ }\vdash{\ } \left(\left(\lambda {\ } \left({\mathtt{\mathbf{x}}}_{3} {\ } \ldots \right) {\ } {\mathtt{\mathbf{t}}}_{4}\right) {\ } {\mathtt{\mathbf{v}}}_{5}\right) {\ }\longrightarrow{\ } \Gamma\left[{\mathtt{\mathbf{x}}}_{1} \mapsto {\mathtt{\mathbf{v}}}_{6}\right]{\ }\vdash{\ } \left(\sigma {\ } {\mathtt{\mathbf{v}}}_{6} {\ } \left(\lambda {\ } \left({\mathtt{\mathbf{x}}}_{3} {\ } \ldots \right) {\ } {\mathtt{\mathbf{t}}}_{4}\right)\right)}}

{\rm E}\text{-}{\rm A {\small PP} S {\small UPERPOSITION}}

 

{{{\left({\mathtt{\mathbf{v}}}_{1} {\ } {\mathtt{\mathbf{v}}}_{3}\right) {\ }\longrightarrow{\ } {\mathtt{\mathbf{t}}}_{13}}} {\qquad} {{\left({\mathtt{\mathbf{v}}}_{2} {\ } {\mathtt{\mathbf{v}}}_{3}\right) {\ }\longrightarrow{\ } {\mathtt{\mathbf{t}}}_{23}}}} \over {{\left(\left(\sigma {\ } {\mathtt{\mathbf{v}}}_{1} {\ } {\mathtt{\mathbf{v}}}_{2}\right) {\ } {\mathtt{\mathbf{v}}}_{3}\right) {\ }\longrightarrow{\ } \left(\sigma {\ } {\mathtt{\mathbf{t}}}_{13} {\ } {\mathtt{\mathbf{t}}}_{23}\right)}}

{\rm E}\text{-}{\rm S {\small UPERPOSITION} R {\small EDUCE} 1}

 

{{{{\mathtt{\mathbf{t}}}_{1} {\ }\longrightarrow{\ } {\mathtt{\mathbf{t}}}_{1} ’}}} \over {{\left(\sigma {\ } {\mathtt{\mathbf{t}}}_{1} {\ } {\mathtt{\mathbf{t}}}_{2}\right) {\ }\longrightarrow{\ } \left(\sigma {\ } {\mathtt{\mathbf{t}}}_{1}’ {\ } {\mathtt{\mathbf{t}}}_{2}\right)}}

{\rm E}\text{-}{\rm S {\small UPERPOSITION} R {\small EDUCE} 2}

 

{{{{\mathtt{\mathbf{t}}}_{2} {\ }\longrightarrow{\ } {\mathtt{\mathbf{t}}}_{2} ’}}} \over {{\left(\sigma {\ } {\mathtt{\mathbf{v}}}_{1} {\ } {\mathtt{\mathbf{t}}}_{2}\right) {\ }\longrightarrow{\ } \left(\sigma {\ } {\mathtt{\mathbf{v}}}_{1} {\ } {\mathtt{\mathbf{t}}}_{2}’\right)}}

{\rm E}\text{-}{\rm S {\small UPERPOSITION} R {\small EDUCE} 3}

 

{} \over {\left(\sigma {\ } \epsilon {\ } {\mathtt{\mathbf{t}}}_{2}\right) {\ }\longrightarrow{\ } {\mathtt{\mathbf{t}}}_{2}}

{\rm E}\text{-}{\rm S {\small UPERPOSITION} R {\small EDUCE} 4}

 

{} \over {\left(\sigma {\ } {\mathtt{\mathbf{t}}}_{1} {\ } \epsilon\right) {\ }\longrightarrow{\ } {\mathtt{\mathbf{t}}}_{1}}