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?


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.

| cite | improve this answer | |
  • $\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$ – Christophe De Troyer Jan 19 '15 at 16:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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