[Haskell-beginners] References for Tarski's High School Algebra Problem, was Re: Cartesian Product in Standard Haskell Libraries

[Jay Sulzberger]

On Mon, 24 Dec 2012, Jay Sulzberger wrote:

>
>
> On Mon, 24 Dec 2012, Kim-Ee Yeoh <ky3 at atamo.com> wrote:
>
>>> the result is of type [()] but for a cartesian n-product, you would like
>> [[a]]
>> 
>> Right. So what we have here is a product over a count of 0 sets, which is
>> isomorphic to the function space that has the null set as domain. The
>> latter has exactly one element: the trivial function.
>> 
>> My apologies for misreading what OP wrote:
>> 
>>> This looks to me to be a violation of the rule that the Cartesian
>>> product of an empty list of lists is a list with one element in
>>> it.
>> 
>> I thought he meant something along the lines of sequence ["","x"].
>> 
>> 
>> -- Kim-Ee
>
> Thanks, Kim-Ee!
>
> Your answer and also Chaddai's are very helpful.
>
> I hope to post more in this thread.
>
> oo--JS.

Kim-Ee, I started to write a response answering your first post
in this thread, but then I saw your second.  My intended answer
started by defining some old classic functions, such as binary
append of lists, binary cartesian product of lists, binary + of
non-negative integers, binary * of non-negative integers, and
extending these four binary operations by using fold to get the
usual n-ary extensions of these four operations.  Then I started
to list the most well known identities amongst the four
operations, and the four extended operations, including
identities using various functors defined using the fundamental
map card: FSets -> NNIntegers, where FSets is the collection of
finite sets, ah, this should be length: FLists -> NNIntegers
where FLists is the collection of finite lists and NNIntegers is
the set of non-negative integers.  This morning, I realized I was
headed for a wonderful old problem, which we now see as a
question in New Crazy Types theory: Tarski's High School Algebra
Problem.  Here is some stuff on the problem:

   http://en.wikipedia.org/wiki/Tarski%27s_high_school_algebra_problem
   [page was last modified on 3 May 2012 at 07:37]

   A note by John Baez which also gives some references:
   http://math.ucr.edu/home/baez/week172.html

   A paper by Roberto Di Cosmo and Thomas Dufour which proves that
   Tarski High School Algebra is decidable but not finitely axiomatizable:
   http://www.pps.univ-paris-diderot.fr/~dufour/zeronfa.pdf

   Some notes from 1999 by R. Di Cosmo,
   with pointer to his book on the problem:
   http://www.dicosmo.org/Tarski/Tarski.html

   A note by Thorsten Altenkirch on one of the dependent types case:
   http://www.cs.nott.ac.uk/~txa/publ/unialg.pdf

   R. Gurevic's 1985 paper, which is available for free:
   http://www.ams.org/journals/proc/1985-094-01/S0002-9939-1985-0781071-1/

   A note by S. N. Burris and K. A. Yeats on the history of the problem:
   math.sfu.ca/~kya17/papers/saga_paper4.pdf

and here are some things on zero inputs in the lambda calculus,
one by Todd Trimble, one by John Baez, and one by Peter Selinger:

   http://math.ucr.edu/home/baez/trimble/holodeck.html

   http://math.ucr.edu/home/baez/week240.html

   http://arxiv.org/pdf/1207.6972

oo--JS.


>
>
>> 
>> 
>> On Mon, Dec 24, 2012 at 4:42 PM, Chaddaï Fouché 
>> <chaddai.fouche at gmail.com>wrote:
>> 
>>> On Mon, Dec 24, 2012 at 8:01 AM, Jay Sulzberger <jays at panix.com> wrote:
>>>>
>>>>  > sequence []
>>>>   []
>>>>   it :: [()]
>>>> 
>>>> This looks to me to be a violation of the rule that the Cartesian
>>>> product of an empty list of lists is a list with one element in
>>>> it.  It looks to be a violation because "[]" looks like a name
>>>> for an empty list.  But we also have
>>>>
>>>>  > length (sequence [])
>>>>   1
>>>>   it :: Int
>>>> 
>>>> which almost reassures me.
>>>> 
>>> 
>>> Well the type of the first response is a dead give-away : the result
>>> is of type [()] but for a cartesian n-product, you would like [[a]]
>>> (with a maybe instantiated to a concrete type) ...
>>> What's happening here is that sequence is not "the cartesian
>>> n-product" in general, it is only that in the list monad but in
>>> "sequence []" there's nothing to indicate that we're in the list
>>> monad, so GHC default to the IO monad and unit () so sequence has the
>>> type "[IO ()] -> IO [()]" and there's no IO action in the list
>>> parameter, so there's nothing in the result list.
>>> 
>>> Try :
>>>> sequence [] :: [[Int]]
>>> and you should be reassured.
>>> 
>>> --
>>> Jedaï
>>> 
>>> _______________________________________________
>>> Beginners mailing list
>>> Beginners at haskell.org
>>> http://www.haskell.org/mailman/listinfo/beginners
>>> 
>> 
>
>