The syntax of the algebraic lambda calculus is the following:
- Constant:
@ is the only constant.
- Variable: any identifier
x is a legal variable name.
- Abstraction: for any identifier
x and any term t, [x]t denotes the lambda abstraction.
- Application: for any terms
p and q, (p)q denotes the application of p to q.
- Scalars: for any term
t and for any integers p and q, p*t and p/q*t are valid terms.
- Sum: for any terms
t1, …, tn, |t1+…+tn| denotes the sum of these terms.
We use vertical bars |to delimit it.
The syntax of the resource lambda calculus is the following:
- Constant:
@ is the only constant.
- Variable: any identifier
x is a legal variable name.
- Abstraction: for any identifier
x and any resource term t, [x]t denotes the resource abstraction.
- Bunch: for any resource terms
t1, …, tn,
{t1^m1.….tn^mn} denotes the bunch containing mi occurences
of each ti.
When mi is equal to 1, we just write ti.
- Application: for any resource term
p and any bunch q, <p>q denotes the application of p to q.