Functional logic

Curry, Verse, Flix, Oz, … all functional logic languages.

Values. A value v is either a variable x or a head-normal form hnf. A variable counts as a value because an expression may evaluate to an as-yet-unknown logical variable. A head-normal form hnf is a conventional value. Expressions e include values v and other constructs:

  • sequencing π‘’π‘ž; e. An β€œexpression or equation” π‘’π‘ž is either an ordinary (possibly failing) expression e, or an equation v = e; the syntax ensures that equations can only occur to the left of a β€œ; ”.

  • βˆƒx. e - existential, introduces logical variable

  • fail - yield no values

  • choice e1 || e2 - yield multiple values (e1 followed by e2)

  • one{e} - if e fails, fails, otherwise returns the first of the values yielded by e

  • all{e} - reifies choices as a tuple; n choices mean tuple of length n

A program 𝑝 ::= one{e} is a closed expression e (freevars(𝑒) = βˆ…) taking the first result. If the expression fails, the program fails.

Rewrite rules:

  • βˆƒx1 x2 Β·Β·Β· xn. e means βˆƒx1. βˆƒx2. Β·Β·Β·βˆƒxn. e

  • x := e1; e2 means βˆƒx. x = e1; e2

  • ⟨e1, Β·Β·Β·, en⟩ means x1 := e1; Β·Β·Β·; xn := en; ⟨x1, Β·Β·Β·, xn⟩ where xi are fresh (again skip rebinding values)

  • e1 = e2 means‑ x := e1; x = e2; x where x is fresh (skip if e1 is a value v and the equation is not the last in a sequence)

  • if (βˆƒx1 Β·Β·Β·xn. e1) then e2 else e3 means (one{(βˆƒx1 Β·Β·Β·xn. e1; πœ†βŸ¨βŸ©. e2) || (πœ†βŸ¨βŸ©. e3)})⟨⟩

Note: In the rules marked with a superscript 𝛼, use 𝛼-conversion to satisfy the side condition

A multi-equation pattern match such as:

function pat1 = body1
function pat2 = body2

desugars to

function = Ξ»p.((βˆƒx1 Β·Β·Β· xn. p = pat1; body1) || (βˆƒx1 Β·Β·Β· xn. p = pat2; body2))

Primops and literals:

  • Hnfs include integer constants and primitive operators +, >

  • e1 + e2 means add⟨e1, e2⟩

  • e1 > e2 means gt⟨e1, e2⟩

  • app-add add⟨k1, k2⟩ βˆ’β†’ k3 where π‘˜3 = π‘˜1 + π‘˜2

  • app-gt gt⟨k1, k2⟩ βˆ’β†’ k1 if π‘˜1 > π‘˜2

  • app-gt-fail gt⟨k1, k2⟩ βˆ’β†’ fail if π‘˜1 β©½ π‘˜2

  • u-lit k1 = k2; e βˆ’β†’ e if π‘˜1 = π‘˜2

Lambdas:

  • A head-normal form hnf includes a lambda πœ†x. e.

  • Expressions e include applications v1 v2

  • e1 e2 means f := e1; x := e2; f x, where f,x are fresh (skip rebinding values)

  • πœ†βŸ¨x1, Β·Β·Β·, xn⟩. e means πœ†p. βˆƒx1 Β·Β·Β· xn. p = ⟨x1, Β·Β·Β·, xn⟩; e p fresh, n β©Ύ 0

  • app-beta𝛼 (πœ†x. e) (v) βˆ’β†’ e{v/x} if π‘₯ βˆ‰ fvs(v)

  • u-lambda a=b is stuck if a or b is a lambda

Tuples:

  • A head-normal form includes a tuple ⟨v1, Β·Β·Β·, vn⟩.

  • app-tup ⟨v0, Β·Β·Β·, vn⟩(v) βˆ’β†’ βˆƒx. x = v; (x = 0; v0) || Β·Β·Β· || (x = n; vn) fresh x βˆ‰ fvs(v, v0, Β·Β·Β·, vn)

  • app-tup-0 ⟨⟩(v) βˆ’β†’ fail

  • u-tup ⟨v1, Β·Β·Β·, vn⟩ = ⟨vβ€²1, Β·Β·Β·, vβ€²n⟩; e βˆ’β†’ v1 = vβ€²1; Β·Β·Β·; vn = vβ€²n; e

  • all-choice all{v1 || Β·Β·Β· || vn } βˆ’β†’ ⟨v1, Β·Β·Β·, vn⟩

  • all-value all{v} βˆ’β†’ ⟨v⟩

  • all-fail all{fail} βˆ’β†’ ⟨⟩

Failure:

  • u-fail hnf1 = hnf2; e βˆ’β†’ fail if no unification

  • u-occurs x = V [ x ]; e βˆ’β†’ fail if V β‰  β–‘ (i.e., all but x=x fail)

  • fail-elim 𝑋 [ fail] βˆ’β†’ fail

  • one-fail one{fail} βˆ’β†’ fail

  • choose-r fail || e βˆ’β†’ e

  • choose-l e || fail βˆ’β†’ e

Existential:

  • exi-elim βˆƒx. e βˆ’β†’ e if x βˆ‰ fvs(e)

  • eqn-elim βˆƒx. 𝑋 [ x = v; e ] βˆ’β†’ 𝑋 [ e ] if x βˆ‰ fvs(𝑋 [ e ]) and v β‰  V [ x ]

  • exi-float𝛼 𝑋 [ βˆƒx. e ] βˆ’β†’ βˆƒx. 𝑋 [ e ] if π‘₯ βˆ‰ fvs(𝑋 )

  • exi-swap βˆƒx. βˆƒy. e βˆ’β†’ βˆƒy. βˆƒx. e

Equality:

  • subst 𝑋 [ x = v; e ] βˆ’β†’ (𝑋 {v/x}) [ x = v; e{v/x} ] if v β‰  V [ x ]

  • hnf-swap hnf = v; e βˆ’β†’ v = hnf ; e

  • var-swap y = x; e βˆ’β†’ x = y; e if x β‰Ί y

Sequences:

  • seq-swap π‘’π‘ž; x = v; e βˆ’β†’ x = v; π‘’π‘ž; e unless (π‘’π‘ž is y = vβ€² and y βͺ― x)

  • val-elim v; e βˆ’β†’ e

  • seq-assoc (π‘’π‘ž; e1); e2 βˆ’β†’ π‘’π‘ž; (e1; e2)

  • eqn-float v = (π‘’π‘ž; e1); e2 βˆ’β†’ π‘’π‘ž; (v = e1; e2)

Choice:

  • one-value one{v} βˆ’β†’ v

  • one-choice one{v || e} βˆ’β†’ v

  • choose-assoc (e1 || e2) || e3 βˆ’β†’ e1 || (e2 || e3)

  • choose SX [𝐢𝑋 [ e1 || e2 ] ] βˆ’β†’ SX [𝐢𝑋 [ e1 ] || 𝐢𝑋 [ e2 ] ]