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.

enter image description here

Could somebody help me understand what rule pur7 means?


1 Answer 1


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.

  • $\begingroup$ 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! $\endgroup$ Jan 19, 2015 at 16:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.