Exploratory Functions on Nondeterministic Strategies, up to Lower Bisimilarity

We consider a typed lambda-calculus with no function types, only alternating sum and product types, so that closed terms represent strategies. We add nondeterminism and consider strategies up to lower (i.e. divergence-insensitive) bisimilarity. We investigate the question: when is a function on strategies definable by an open term (with sufficiently large nondeterminism)?The answer is: when it is “exploratory”. This is a kind of iterated continuity property, coinductively defined, that is decidable in the case of a function between finite types.In particular, any exploratory function between countably nondeterministic strategies is definable by a continuum nondeterministic term.