home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #31 / NN_1992_31.iso / spool / comp / lang / function / 1481 < prev    next >
Encoding:
Text File  |  1992-12-22  |  3.6 KB  |  87 lines
  1. Newsgroups: comp.lang.functional
  2. Path: sparky!uunet!zaphod.mps.ohio-state.edu!rpi!ghost.dsi.unimi.it!univ-lyon1.fr!chx400!josef!cap
  3. From: cap@ifi.unizh.ch (Clemens Cap)
  4. Subject: Higher recursion
  5. Message-ID: <1992Dec22.153733.5374@ifi.unizh.ch>
  6. Followup-To:  poster
  7. Sender: cap@ifi.unizh.ch
  8. Organization: University of Zurich, Department of Computer Science
  9. Date: Tue, 22 Dec 92 15:37:33 GMT
  10. Lines: 75
  11.  
  12.  
  13.         Desperately seeking 
  14.         
  15.       ***************************************
  16.       *help (examples, references, pointers)*
  17.       ***************************************
  18.  
  19.       for higher order recursion theory.
  20.  
  21.  
  22. Introdution
  23. ************
  24.  
  25. In classical recursion theory one studies questions like the following:
  26.  
  27. A functional F is a function from partial recursive functions to partial 
  28. recursive functions.
  29.  
  30. A functional F is called effective, iff there exists an extensional, partial 
  31. recursive function h, such that the effect functional F has on a function g
  32. can be described by an action of this function h on an arbitrary program q
  33. of this function g.
  34.  
  35. A functional F is called monotonic, iff whenever for two functions f and g 
  36. there is f < g, then also F(f) < F(g).  ( < is the usual ordering of partial 
  37. functions).
  38.  
  39. A functional F is called compact, iff for every function f there exists 
  40. a function u with finite domain and u < f, such that F(f) = F(u).
  41.  
  42. Classical recursion theory now studies the following questions:
  43.  
  44. (0) A functional is continuous, iff it is monotonic and compact.
  45. (1) A functional is effective, iff it is continuous.
  46. (2) A functional having the properties of (1) (and (2) always has a least
  47. fixed point function m (so F(m) = m), which can effectively be calculated
  48. either by inductive techniques or by applying a suitable recursive function
  49. to a program of the extensional function belonging to the functional, thus
  50. leading to a program of the least fixed point m.
  51.  
  52. **********************
  53. Now comes my QUESTION:
  54. **********************
  55.  
  56. A) Is there an analogon to this for functionals of higher type?
  57.    For example, let us call a functional of type-2 an operation which takes
  58.    a number of ordinary functionals (as defined above) as argument 
  59.    and yields an ordinary functional as result.
  60.    What can be said about representations via programs, or extensional
  61.    functions, about continuity, monotonicity and compactness ?
  62.    Is there an analogon to above theorem from type-1 recursion theory ?
  63.    
  64. B) G. Plotkin writes in his lecture notes on domains on page 6 
  65.    "And indeed at higher types continuity is a real restriction."
  66.    I would like to understand the meaning of this sentence in the context of
  67.    above lines and I am looking for a concrete example.
  68.    
  69. C) I have studied Kechris and Moschovakis on "Recursion in Higher Types" in
  70.    the Handbook of Mathematical Logic by Barwise, and found some pointers.
  71.    However, I am interested essentially in "real computable and constructive"
  72.    stuff -- everything should have some consequences for a programmer sitting
  73.    in front of his Turing Machine. So also I am very happy for help along the
  74.    line of "fully-abstract-categoric-domain-theoretical-stuff" I would even be
  75.    more happy with help along the line of "apply-example-program-useful-recursive"
  76.    
  77.  
  78. Replies please to cap@ifi.unizh.ch.
  79. I will post a summary on comp.theory, if there are interesting replies.
  80.  
  81. Happy Xmas to the Usenet.
  82. -- 
  83. * Dr. Clemens H. CAP                        cap@ifi.unizh.ch (email)   
  84. * Ass. Professor for Formal Methods in CS   +(1) 257-4326    (office)
  85. * Dept. of Computer Science                 +(1) 322 02 19   (home)
  86. * University of Zurich                      +(1) 363 00 35   (fax) 
  87.