Dear Vaughan, i should mention that for the type, M[=E2=88=82=C2=B5Mx=C2=B5M,=C2=B5M], to b= e inhabited you need some way to bottom out the recursion. In the reflective= higher-order pi-calculus that corresponds to the constant summand, 1, repre= senting the stopped process.=20 For the lambda calculus you need to do something similar -- like add in an e= xplicit distinguished representation of divergence, or add in some ground te= rms, like the booleans.=20 More generally, the trick needs to employ the option monad if the type is is= o to 1+N for appropriate N. i'm happy to provide either Haskell or Scala code to illustrate that the pro= cedure is effective. i can also provide OCaml code, but it's considerably mo= re verbose and painful to write. Best wishes, --greg Managing Partner Biosimilarity LLC [For admin and other information see: http://www.mta.ca/~cat-dist/ ]