Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.



Re: This Week's Finds in Mathematical Physics (Week 240)
Posted:
Oct 26, 2006 12:14 PM


In article <ehmgfb$mdr$1@news.ks.uiuc.edu>, Esa A E Peuha <esa.peuha@helsinki.fi> wrote:
>baez@math.removethis.ucr.andthis.edu (John Baez) writes:
>> In analysis, X^Y >> can approach anything between 0 and 1 when X and Y approach 0.
>If X^Y approaches Z, then X^(Y) appoaches 1/Z, so the actual range of >possible values is between 0 and infinity, including both endpoints.
I was imagining both X and Y being positive, perhaps because I had set theory on my mind, and sets have a nonnegative number of elements. :) But, of you're right if Y can be negative.
Here are some other corrections and comments, which have been used to improve the web version of "week240", available here:
http://math.ucr.edu/home/baez/week240.html
When I wrote the first version of this Week's Finds, I was ignorant of work before Dolan and Trimble's that also described the free cartesian closed category on one object in terms of games. I was gently set straight by Dominic Hughes, who has permitted me to attach this post of his from the category theory mailing list:
This "backtracking game" characterisation has been known since around '93'94, in the work of Hyland and Ong:
M. Hyland and L. Ong. On full abstraction for PCF. Information and Computation, Volume 163, pp. 285408, December 2000. [Under review for 6 years!] ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Luke.Ong/pcf.ps.gz
(PCF is an extension of typed lambda calculus.) My D.Phil. thesis extended the lambda calculus (free CCC) characterisation to secondorder, published in:
Games and Definability for System F. Logic in Computer Science, 1997 http://boole.stanford.edu/~dominic/papers/
To characterise the free CCC on an *arbitrary* set {Z,Y,X,...} of generators (rather than a single generator, as you discuss), one simply adds the following Copycat Condition:
(*) Whenever first player plays an occurrence of X, the second player must play an occurrence of X.
[Try it: see how X > Y > X has just one winning strategy.] Although the LICS'97 paper cited above appears to be the first place the Copycat Condition appears in print, I like to think it was already understood at the time by people working in the area. Technically speaking, winning strategies correspond to etaexpanded betanormal forms. See pages 57 of my thesis for an informal description of the correspondence.
It sounds like you've reached the point of trying to figure out how composition should work. Proving associativity is fiddly. Hyland and Ong give a very elegant treatment, via a larger CCC of games in which *both* players can backtrack. The free CCC subcategory is carved out as the socalled *innocent* strategies. This composition is almost identical to that presented by Coquand in:
A semantics of evidence for classical arithmetic. Thierry Coquand. Proceedings of the CLICS workshop, Aarhus, 1992.
Dominic
PS A gametheoretic characterisation with an entirely different flavour (winning strategies less "obviously" corresponding to etalong betanormal forms) is:
Abramsky, S., Jagadeesan, R. and Malacaria, P., Full Abstraction for PCF. Info. & Comp. 163 (2000), 409470. http://web.comlab.ox.ac.uk/oucl/work/samson.abramsky/pcf.pdf [Announced concurrently with HylandOng, around '93'94.]
On a different subject, James Dolan had this to say:
you describe holodeck strategies for "lady or tiger" where you take back "just when the tiger is about to eat you", but that's not the way it works. you take back just _after_ the tiger has eaten you.
(i guess that this is partially because of your lack of experience with computer games with a "saved game" feature. typically you die in the game and the computer plays some sort of funeral or at least funereal music; then you're taken to the reincarnation gallery where you select one to return to from your catalog of previous lives. or something like that.)
Also, in the first version of this Week's Finds I claimed that all systematic ways of picking an element of (X^X)^(X^X) could be defined using the lambda calculus. I was disabused of this notion by Vaughan Pratt, who wrote:
Hi, John,
In "week240", you said
The moral of this game is that all systematic methods for picking an element of (X^X)^(X^X) for an unknown set X can be written using the lambda calculus.
What is unsystematic about the contagiousfixpoint functional? This is the functional that maps those functions that have any fixpoints to the identity function (the function that makes every element a fixpoint) and functions without fixpoints to themselves (thus preserving the absence of fixpoints). It's a perfectly good functional that is equally well defined for all sets X, its statement in no way depends on X, and conceptually the concept of contagious fixpoints is even intuitively natural, but how do you write it using the lambda calculus?
Many more examples in this vein at JPAA 128, 3392 (Pare and Roman, Dinatural numbers, 1998). The above is the case K = {0} of Freyd's (proper) class of examples.
Vaughan
Here Pratt uses "functional" to mean what I was calling an "operator".
Finally, Tom Payne at UCR coaxed me into using more standard lambda calculus notation.
.........................................................................
Puzzle 29: Stravinsky's Rite of Spring caused a ruckus in Paris, but which piece actually got him *arrested* in Boston?
If you get stuck, try:
http://math.ucr.edu/home/baez/puzzles/



