# Lambda Calculus Notation

I'm reading through the paper Transactors: A Programming Model for Maintaining Globally Consistent Distributed State in Unreliable Environments by John Field and Carlos Varela.

I have basic knowledge about the lambda calculus (typed lambda calculus to be more precise) thanks to a class I took at my university.

However, I'm stuck finding out what the rule shown below actually means. I have looked through the Types and Programming Languages book by Benjamin Pierce but I can't seem to find an explanation.

Could somebody help me understand what rule pur7 means?

It probably depends on what $\mathcal{F}$ is -- the text tells you.
Each $f\in\mathcal{F}$ is a build-in/primitive function (such as $+$) and [pur7] gives the result of applying it to some arguments. $[\![ f]\!]$ gives the semantic interpretation of the function, and applying that to the arguments $v_1,\ldots,v_n$ gives the result of the function.