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

[Jay Sulzberger]

On Wed, 26 Dec 2012, Kim-Ee Yeoh <ky3 at atamo.com> wrote:

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

Thanks, Kim-Ee!

I was not directly asking a question in the post.

>
> 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.

Yes.  This is not stupid, and I had been thinking a bit about
such a thing before I saw Di Cosmo's stuff.

There was last semester a course at Columbia on "Big Data".  I
never attended any of it but read Cathy O'Neil's blog posts about
it at

   http://mathbabe.org

I thought that a good project for the class would be to attempt
to make a search engine for code.  Now I'd want the search engine
to be able to classify two programs in two different programming
systems, say Basic and Scheme, or C and Haskell, as "being the
same program", even if their source code does not use the same
names for things.  Of course, the general principle that gross
human language word similarities gets you a lot, will hold here
too.  The interesting case would be if we stripped away all
comment, and surrounding text, and then tried to do the
grouping/indexing.  Note that this does not, at least at first,
look like the sort of thing one does in, ah, econometrics, nor in
most computer helped "market research".  I know that there has
been some work on the problem.

>
> 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))

I will have to read this carefully, but I know the general
problem ;)

> ...
>
> ?
>
> Cue Tarski's HSA problem.

Yes.

>
>
>
> -- Kim-Ee

I will attempt to post more, and this time I will put some
elementary, very elementary, Haskell code in, showing what GHCi
tells me about sequence just as you and Chaddai have said to do.

oo--JS.


>
>
> 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
>>
>>
>