Post #1889741
2026-04-23 18:15 UTC
@carloangiuli Except that "ω-" is a distraction, because we don't really need it anywhere when reasoning about PCF programs. 🙂
Replies (1)
-
@MartinEscardo@mathstodon.xyz 2026-04-23 18:19
@carloangiuli But I do wonder about this, for a long time. Gordon Plotkin proved, using classical mathematics, that an element of a dcpo in the domain of discourse of PCF is computable if and only if it is PCF definable from parallel-or and parallel-exists. Can this be formulated and proved constructively?