I'm reading through the paper Transactors: A Programming Model for MaintainingGlobally Consistent Distributed State in UnreliableEnvironments 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?
Lambda Calculus Notation
lambda calculus
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.