Nondeterminism

A classic example of a computational effect that isn’t part of most programming languages is nondeterminism. Prolog has something like it, and some Schemes have it [1:4.3]. Probabilistic programming is closely related.

Syntax and examples

Assume that we have lists (TAPL 11.12), including the syntactic sugar

      [] ≡ nil
    [t1] ≡ cons t1 nil
[t1, t2] ≡ cons t1 (cons t2 nil)

and so on. We write infix ++ for list concatenation.

The new syntax for nondeterminism is:

t ::= ...
      collect t
      amb t1 t2
      fail

amb takes two arguments and causes evaluation to fork into two branches, one for each argument.

fail causes the current branch of evaluation to fail.

collect collects all the non-failed branches and puts their values into a list.

For example, if you have a nickel, a dime, and a quarter, and want to know all the amounts you can pay exactly, it’s

collect ((amb 0 5) + (amb 0 10) + (amb 0 25))
⟶* [0, 25, 10, 35, 5, 30, 15, 40]

If this reminds you of Python’s

[n+d+q for n in [0, 5] for d in [0, 10] for q in [0, 25]]

you’re right. But amb can do some things that would be difficult with list comprehensions, like a function that takes a list of coin values and produces all possible sums:

sums ≡ fix λs. λc. if isnil c then 0 else amb 0 (car c) + s (cdr c)
collect (sums [5, 10, 25]) ⟶* [0, 25, 10, 35, 5, 30, 15, 40]

Typing and evaluation

      Γ ⊢ t : T
――――――――――――――――――――――
Γ ⊢ collect t : List T

Γ ⊢ t1 : T   Γ ⊢ t2 : T
―――――――――――――――――――――――
   Γ ⊢ amb t1 t2 : T

――――――――――――
Γ ⊢ fail : T

When defining the semantics of try, we had to define two kinds of evaluation contexts, and we must do the same thing here for collect. An F context cannot break through collect, but an E can.

F ::= [⋅]
      F t
      v F
      amb F t
      amb v F

E ::= F
      F[E]
      collect E

The evaluation rules look simple, but think carefully about them.

                   collect v ⟶ [v]
        collect F[amb v1 v2] ⟶ collect F[v1] ++ collect F[v2]
             collect F[fail] ⟶ []

Example:

collect ((amb 0 5) + (amb 0 10))
⟶ [collect (0 + (amb 0 10)] ++ [collect (5 + (amb 0 10)]
⟶ [collect (0 + 0)] ++ [collect (0 + 10)] ++ [collect (5 + (amb 0 10)]
⟶ [collect 0] ++ [collect (0 + 10)] ++ [collect (5 + (amb 0 10)]
⟶ [0] ++ [collect (0 + 10)] ++ [collect (5 + (amb 0 10)]
⟶* [0, 10, 5, 15]

In pure lambda calculus

Unsurprisingly, we can convert lambda calculus with collect and amb into pure lambda calculus.

Terms that don’t have nondeterminism transform into singleton lists.

    𝒯⟦x⟧ = [x]
𝒯⟦λx. t⟧ = [λx. 𝒯⟦t⟧]

But amb and fail transform into other kinds of lists.

𝒯⟦amb x1 x2⟧ = x1 ++ x2
     𝒯⟦fail⟧ = []
𝒯⟦collect t⟧ = 𝒯⟦t⟧

Application of one variable to another is easy, as before.

𝒯⟦x1 x2⟧ = x1 x2

And as before, the translation of let is the trickiest:

𝒯⟦let x = t1 in t2⟧ = flatmap (λx. 𝒯⟦t2⟧) 𝒯⟦t1⟧

where flatmap f l applies f to every element of l to get a list of lists. Then it concatenates all those lists together.

flatmap ≡ fix λfm. λf. λl. if isnil l then nil else (f (car l)) ++ (fm f (cdr l))

Now we can define more general translations for amb and applications:

𝒯⟦amb t1 t2⟧ = 𝒯⟦let x1 = t1 in let x2 = t2 in amb x1 x2⟧
             = flatmap (λx1. flatmap (λx2. x1 ++ x2) 𝒯⟦t2⟧) 𝒯⟦t1⟧
    𝒯⟦t1 t2⟧ = 𝒯⟦let x1 = t1 in let x2 = t2 in x1 x2⟧
             = flatmap (λx1. flatmap (λx2. x1 x2) 𝒯⟦t2⟧) 𝒯⟦t1⟧

References