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 tamb 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))