Full syntax of λλ (from the paper):<p><pre><code> e ::= v | x | input(p)
| let x = e1 in e2
| (e1, e2)
| unpack e1 as (x1, x2) in e2
| phase(θ, e)
| split(r, e)
| unitary(U, (e1, e2))
| output(p) <- e1; e2
v ::= r ↓ ℝ | p ↓ Port | U ↓ Unitary | ()
τ ::= ℝ | Port | Opt | Unitary | Unit |(τ1 * τ2)</code></pre>
Note that this is not an extension of the pure λ-calculus.<p>Abstraction (λx.e) and application (f a) are missing,
although the let construct "let x = e1 in e2" is equivalent to their combination
((λx.e2) e1).<p>The paper has few details on the higher-level specification language in which users specify desired behaviour:<p>> Specification Language. Specifications are written as relations between input and output ports, expressed using linear expressions. On their own, specifications are not λ _λ programs. It is the job of the synthesizer to find λ _λ programs that realize a given specification. For example, a simple switching behavior can be specified as output[i] = input[j], while a 2x2 AllReduce operation can be written as output[1] = (input[1] + input[2])/sqrt(2) and output[2]= (input[1] - input[2])/sqrt(2).
So simplified, a bit like System F.