# Nondeterminism

A classic example of a computational effect that isn’t part of most programming languages is nondeterminism. (Prolog has something like it.)

## Syntax and examples

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

``````      [] ≡ 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 t``````

`amb` takes a list of n arguments and causes evaluation to fork into n branches, one for each value in the list.

`collect` collects all the 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

Γ ⊢ t : List T
——————————————
Γ ⊢ amb t : T

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

E ::= ...
amb E
collect E

collect v ⟶ [v]
collect F[amb [v1, v2, ...]] ⟶ collect F[v1] ++ collect F[v2] ++ ...``````

## In pure lambda calculus

We can convert lambda calculus with `collect` and `amb` into pure lambda calculus:

``````𝒯⟦x⟧ = [x]
𝒯⟦nil⟧ = [nil]
𝒯⟦cons⟧ = [cons]

𝒯⟦λx. t⟧ = [λx. 𝒯⟦t⟧]
𝒯⟦t1 t2⟧ = concat (map (λf. concat (map f 𝒯⟦t2⟧)) 𝒯⟦t1⟧)
𝒯⟦amb t⟧ = concat 𝒯⟦t⟧
𝒯⟦collect t⟧ = [𝒯⟦t⟧]``````

where `map` and `concat` have their usual meanings, but for completeness, we can define them as:

``````map ≡ fix λm. λf. λx. if isnil x then nil else cons (f (car x)) (m f (cdr x))
concat ≡ fix λc. λx. if isnil x then nil else (car x) ++ (c (cdr x))``````