I'm designing a language which implements lambda calculus and (first-order) predicate calculus, where lambdas behave as the abstraction encapsulating logic, compositionally forming a computational model for higher-order logic.

How does one, in general, choose between operational, denotational, and axiomatic semantics? I understand the way in which they describe the semantics for some language specification, and I understand they're often mixed (particularly operational semantics with one of the other two), but I'm not sure how to best identify the right formal semantics to use in general. I've seen lambda calculus expressed in both operational and denotational semantics (purely), for instance. I'm currently favoring denotational semantics for my project. But I would like to know how to identify whether this is the right choice for this project and others in the future.

I've read that denotational semantics is useful in source-to-source translation, which is what I'm thinking of doing: either writing an interpreter or a transpiler (source-to-source compiler), which translates the code into C++ and allow a C++ compiler handle the compilation into machine code. The idea is that I can make use of lambdas in C++ (since C++11), as they are standard/portable and rigorous. I'm leaning towards the compiler currently. Or might this not be a good idea? I may write something better later on with LLVM or GNU Lightning.

An additional question (if anyone can answer this as well, that would be great!)
I understand how environments / environment functions are necessary when interpreting a language that needs to keep track of variables and such, but is it necessary/applicable for a compiler? If so, how would the environment be best expressed/implemented if I were to compile to C++? By environment, I mean the set of paired values which map identifiers to values.

  • $\begingroup$ "How does one, in general, choose between operational, denotational, and axiomatic semantics? " -- How does one choose, in general, between a spoon, a fork, and a knife? There are no general rules: you have to inspect what you are going to do for each case, and pick the tool that fits the requirements best. $\endgroup$
    – Raphael
    Sep 2, 2017 at 7:24
  • $\begingroup$ You use a spoon, fork, or knife depending on the food. I would argue there absolutely are general rules. For instance, you need both a fork and knife to cut meat such as steak, and you need a spoon for food like soup. Fairly general. In any case, I expect that someone would outline how each type of formal semantics fits with respect to sets of requirements. That is essentially a set of general rules. $\endgroup$
    – Phizo
    Sep 2, 2017 at 7:48
  • $\begingroup$ So you're inventing HOL? $\endgroup$ Sep 2, 2017 at 16:29
  • $\begingroup$ No. That isn't the intention. Nor will it be the product. $\endgroup$
    – Phizo
    Sep 2, 2017 at 17:10


Your Answer

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

Browse other questions tagged or ask your own question.