# 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.

• I was just spitting through the text but you beat me to it! It is indeed the case. I should have checked all the definitions. Thank you for clarifying, it is much appreciated! Jan 19, 2015 at 16:53