2
$\begingroup$

I was looking at some slides of John Longley's here, where he mentions "the Kierstead functional"

$$\lambda f.f(\lambda x.f(\lambda y.x)) \ ,$$

(where $f$ should be of type $2$, and $x,y$ of ground type, so a functional of type $3$).

After ten or fifteen minutes of googling around I could only find that this must be the Kierstead in question, but not much else, other than that "Kierstead terms" have provided handy examples for certain notions of "safety" (see Example 1.5 here) or "innocence" (see section 2.3.1, here).

My questions: What is the origin of these lambda terms, that is, to which work of Kierstead can they be traced back? Are there other examples of their use in the literature?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
2
$\begingroup$

This example (or a very similar one) first appeared in the literature in Kleene's paper 'Recursive functionals and quantifiers of finite types revisited I' (Proc. Generalized Recursion Theory II, Oslo) in 1978. Here Kleene attributes the example to his student Kierstead.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Oops, I was writing up what I found while you were answering. Thanks for the pointer. It goes further back than "Recursive functionals and quantifiers of finite types revisited II" then... $\endgroup$
    – Basil
    Commented Sep 24, 2014 at 10:14
3
$\begingroup$

Okay, it was not a fifteen minutes thing, but a couple-of-hours one (for me).

The Kierstead person in question is not the one I link to in the OP, but David Philip Kierstead, a student of Kleene (who seems to have fallen off the radar for some reason).

The above type $3$ functional appeared as Example 3.6 in [Kierstead 1980], as a counterexample to a sequentiality conjecture of Kleene's regarding higher-type oracles, namely that a (nonconstant) type $3$ oracle should be able to provide a type $1$ input to its type $2$ argument. This was an expectation based on lower-type intuition, and is refuted by the circularity caused by $f$ in the functional of Kierstead.

Kleene himself discusses the problem raised by this counterexample in [Kleene 1980] (in the same proceedings tome where Kierstead's paper appeared), in section 8.2. A good and more intuitive account of the issue is given by Longley again, in section 4.1.2 of [Longley 2005]; this is where I started unraveling the whole story.

(Next time I'll wait for a day before I pose a question.)

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .