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

[Kim-Ee Yeoh]

Jay, I appreciate your references. I'm not sure whether you're asking a
question this time around.

I've skimmed some of Di Cosmo's work, and I particularly liked the type
isomorphism narrative as applied to a queryable database of functions.

Anyone who has used Hayoo or Hoogle enough encounters the problem of
non-canonicity of type signatures. Which of the following isomorphic
signatures should we search for

(a, Either a b) -> (s,c)
((a,a)->(s,c), (a,b)->(s,c))
(a->a->(s,c), a->b->(s,c))
(a->a->s, a->a->c, a->b->(s,c))
...

?

Cue Tarski's HSA problem.



-- Kim-Ee


On Wed, Dec 26, 2012 at 5:56 AM, Jay Sulzberger <jays at panix.com> wrote:

>
>
> 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<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<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<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<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<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/<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<http://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/trimble/holodeck.html>
>
>   http://math.ucr.edu/home/baez/**week240.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<http://www.haskell.org/mailman/listinfo/beginners>
>>>>
>>>>
>>>
>>
>>
>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20121226/ba37654f/attachment.htm>