🚀 go-pugleaf

		Desperately seeking 
		
      ***************************************
      *help (examples, references, pointers)*
      ***************************************

	  for higher order recursion theory.


Introdution
************

In classical recursion theory one studies questions like the following:

A functional F is a function from partial recursive functions to partial 
recursive functions.

A functional F is called effective, iff there exists an extensional, partial 
recursive function h, such that the effect functional F has on a function g
can be described by an action of this function h on an arbitrary program q
of this function g.

A functional F is called monotonic, iff whenever for two functions f and g 
there is f < g, then also F(f) < F(g).  ( < is the usual ordering of partial 
functions).

A functional F is called compact, iff for every function f there exists 
a function u with finite domain and u < f, such that F(f) = F(u).

Classical recursion theory now studies the following questions:

(0) A functional is continuous, iff it is monotonic and compact.
(1) A functional is effective, iff it is continuous.
(2) A functional having the properties of (1) (and (2) always has a least
fixed point function m (so F(m) = m), which can effectively be calculated
either by inductive techniques or by applying a suitable recursive function
to a program of the extensional function belonging to the functional, thus
leading to a program of the least fixed point m.

**********************
Now comes my QUESTION:
**********************

A) Is there an analogon to this for functionals of higher type?
   For example, let us call a functional of type-2 an operation which takes
   a number of ordinary functionals (as defined above) as argument 
   and yields an ordinary functional as result.
   What can be said about representations via programs, or extensional
   functions, about continuity, monotonicity and compactness ?
   Is there an analogon to above theorem from type-1 recursion theory ?
   
B) G. Plotkin writes in his lecture notes on domains on page 6 
   "And indeed at higher types continuity is a real restriction."
   I would like to understand the meaning of this sentence in the context of
   above lines and I am looking for a concrete example.
   
C) I have studied Kechris and Moschovakis on "Recursion in Higher Types" in
   the Handbook of Mathematical Logic by Barwise, and found some pointers.
   However, I am interested essentially in "real computable and constructive"
   stuff -- everything should have some consequences for a programmer sitting
   in front of his Turing Machine. So also I am very happy for help along the
   line of "fully-abstract-categoric-domain-theoretical-stuff" I would even be
   more happy with help along the line of "apply-example-program-useful-recursive"
   

**** Please mail to cap@ifi.unizh.ch
     I will post a summary, in case I receive interesting pointers.

Thanx, and happy holidays (after having answered my questions, of coures (;-) )



-- 
* Dr. Clemens H. CAP                        cap@ifi.unizh.ch (email)   
* Ass. Professor for Formal Methods in CS   +(1) 257-4326    (office)
* Dept. of Computer Science                 +(1) 322 02 19   (home)
* University of Zurich                      +(1) 363 00 35   (fax)