Back to News
Advertisement
Advertisement

⚡ Community Insights

Discussion Sentiment

50% Positive

Analyzed from 157 words in the discussion.

Trending Topics

#input#output#paper#language#let#unitary#specification#port#calculus#specifications

Discussion (5 Comments)Read Original on HackerNews

deepsunabout 2 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)
trompabout 2 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).

pjmlpabout 1 hour ago
So simplified, a bit like System F.
trompabout 2 hours ago
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.

ktallett27 minutes 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?