The second λ is subscripted. As footnote 1 in the paper says:
> Pronounced “lambda lambda”. One λ refers to the λ-calculus and the other refers to an optical wavelength.
deepsun 3 hours ago [-]
Full syntax of λλ (from the paper):
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)
tromp 3 hours ago [-]
Note that this is not an extension of the pure λ-calculus.
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).
The paper has few details on the higher-level specification language in which users specify desired behaviour:
> 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).
pjmlp 2 hours ago [-]
So simplified, a bit like System F.
ktallett 2 hours ago [-]
I am curious why develop a new language instead of building a library for an existing language. What are the benefits as I didn't see this in the paper? Can it interact with other languages?
black_knight 1 hours ago [-]
The first sentence of the abstract gives a motivation: "λλ uses a linear type system to encode the physical constraints of optics, rejecting unrealizable programs at compile time."
The fact that it its own language does not preclude using it within the context of a different language. You can embed a domain specific language into a general purpose one.
Rendered at 11:35:59 GMT+0000 (Coordinated Universal Time) with Vercel.
> Pronounced “lambda lambda”. One λ refers to the λ-calculus and the other refers to an optical wavelength.
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).
The paper has few details on the higher-level specification language in which users specify desired behaviour:
> 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).
The fact that it its own language does not preclude using it within the context of a different language. You can embed a domain specific language into a general purpose one.