Interdefinability of Parallel Operations in PCF

• To: types@theory.LCS.MIT.EDU
• Subject: Interdefinability of Parallel Operations in PCF
• From: Allen Stoughton <allen%cogs.sussex.ac.uk@nsfnet-relay.ac.uk>
• Date: Mon, 31 Jul 89 11:03:00 EDT
• Sender: meyer@theory.LCS.MIT.EDU

Date: Mon, 31 Jul 89 13:34:04 BST

           Interdefinability of Parallel Operations in PCF

I have just shown that the parallel conditional over the natural
numbers (pif_iota) can be defined from parallel or (por).  This has
the consequence that por, pif_iota and pif_o (parallel conditional
over the booleans) are interdefinable elements of the continuous
function model of PCF.  (See Plotkin's paper, "LCF considered as a
programming language", for definitions and notation.)

One defines

    PIf_iota = Y_sigma F 0 ,

where sigma = iota -> o -> iota -> iota -> iota, and

    F = lambda fnxyz.
        If_iota (POr (PAnd (Eq y n) (Eq z n))
                     (PAnd x (Eq y n))
                     (PAnd (Not x) (Eq z n)))
                n
                (f (+1 n) x y z) .

Here, Not is negation, we have extended POr to three arguments in
the obvious way, PAnd is the "parallel and" operation, dual to
POr, and Eq is the equality test for the natural numbers.

The above definition makes use of ideas from the (independent) proofs
by Abramsky and Curien that adding parallel or to PCF is enough to
make all isolated elements definable.

To my knowledge this is a new result; any information to the contrary
would be appreciated.

Allen Stoughton

• Prev: Interdefinability of Parallel Operations in PCF
• Next: Sieber's Full-Abstraction for call-by-value (241 lines)
• Index(es):
  • Main
  • Thread