3
$\begingroup$

I wonder if there exist topologies for the lambda-calculus where computational divergence (like for $\Omega = (\lambda x. x x) (\lambda x. x x)$) has a topological meaning as the divergence of a sequence.

Unfortunately, I'm unfamiliar with the models and topologies studied on the lambda-caculus. Thus, my question.

$\endgroup$
  • $\begingroup$ You already linked to literature that contains a wealth of material about your question, and stated you're not familiar with it. I am very sorry, but this is not a research-level quesiton (even without your remarks, it's a basic fact of denotational semantics that termination is an open property). Please ask on cs.stackexchange.com, where it is appropriate to explain such things. $\endgroup$ – Andrej Bauer Nov 13 '19 at 12:11
  • $\begingroup$ @AndrejBauer thank you for your suggestion. To clarify, by "open property" you mean something for which we don't have an answer? $\endgroup$ – Rodrigo Nov 13 '19 at 12:35
  • $\begingroup$ What I mean is that the set of programs which terminate forms an open set (under a suitable topology, look up "Scott topology"). $\endgroup$ – Andrej Bauer Nov 13 '19 at 13:45

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.