9
$\begingroup$

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?

$\endgroup$

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
  • 3
    $\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
  • 1
    $\begingroup$ About Löwenheim–Skolem in particular, IIRC proving Löwenheim–Skolem depends on some axiom of choice, so it doesn't really tell you anything interesting, all it says is: if a model $M$ exist, then a crazy model $M'$ of any chosen cardinality exists. But you have no idea what $M'$ looks like, as Choice is not constructive. This says more about ZF's inability to nail down infinities, than about the fine-structure of higher-order computation. $\endgroup$ – Martin Berger Nov 26 '18 at 13:52
  • 3
    $\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 agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.