Denotational semantics interpret the theories of various lambda calculi in various (set-theoretic, domain-theoretic, category-theoretic, game...) models. Let $T$ be the theory of one such lambda calculus $\lambda_?$. If I understand correctly, a denotational semantics for $\lambda_?$ is thus just a model for $T$.

The question here is, have applying the tools and methods of model theory to denotational semantics yielded useful results. For example, what does the Löwenheim–Skolem theorem tell us about the denotational semantics of various lambda calculi?


migrated from cs.stackexchange.com Nov 26 '18 at 5:06

This question came from our site for students, researchers and practitioners of computer science.

  • $\begingroup$ I suspect the Lowenheim-Skolem theorem is irrelevant here, since - if I understand correctly - one generally cares about term models, and these are always countable already. $\endgroup$ – Noah Schweber Nov 25 '18 at 20:23
  • $\begingroup$ @NoahSchweber I also doubt if the Lowenheim-Skolem theorem is useful here. But as you said, if there are countable models, there should be uncountable models as well, so maybe it's interesting to look at what those models are? $\endgroup$ – xuq01 Nov 25 '18 at 22:29
  • 2
    $\begingroup$ @NoahSchweber, in denotational semantics term models is what you want to get away from. $\endgroup$ – Martin Berger Nov 26 '18 at 10:21
  • 2
    $\begingroup$ I doubt that traditional model theory can directly be used in models lambda-calculus, because the latter is higher-order, while most model-theory is model theory of first-order logic. For example John Reynolds proved (in his Polymorphism is not set-theoretic) that there cannot be conventional models of the polymorphic lambda-calculus. $\endgroup$ – Martin Berger Nov 26 '18 at 10:26
  • 2
    $\begingroup$ I don't know if you'd consider this denotational semantics, but the way we relate program logics and other semantics is basically (simplifying a bit) elementary equivalence from model theory: let's assume you have some program logic (e.g. Hoare triples, or Hennessy–Milner logic). Then you define an equivalence of programs using EE by saying $P \cong Q$ if for all formulae $\phi$ of the logic we have: $P \models \phi$ iff $Q \models \phi$. Now you want to show that if you have some other equivalence $\equiv$ on programs: $\cong$ and $\equiv$ coincide. $\endgroup$ – Martin Berger Nov 26 '18 at 14:01

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.