Elektrine lite

← Feed

@mevenlennonbertrand@lipn.info

Post #4119651

2026-05-29 12:27 UTC

@rntz@recurse.social Don't we have pand x y = (not (por (not x) (not y))? In general, parallel or is all you need for the "standard" denotational semantics of PCF in domains to be fully abstract, so in a sense it gives you "all the parallelism you need", and other similar constructs like your pand should be definable from it.

Replies (2)

  • @rntz@recurse.social (Technically I'm a bit wrong: full abstraction is weaker than definability of all elements of the model, and I don't remember whether this stronger property also holds for the domain model of PCF+por)

    Open ##4119654

  • @rntz@recurse.social 2026-05-29 13:31

    @mevenlennonbertrand@lipn.info indeed, but what if I don't have negation :P (I am less-than-half-joking. If you squint, miniKanren's search strategy implements parallel or. But miniKanren very definitely does not have arbitrary negation. I have heard that Andorra Prolog has something like "parallel and" but I have not investigated further.)

    Open ##4119655