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

Wed Dec 26 07:07:21 CET 2012

On Wed, 26 Dec 2012, Jay Sulzberger wrote:

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

To lay out explicitly what you already know:

The type similarity problem and the code similarity problem are
alike, and one statistical (partial) solution is to run the two
types/programs on the same inputs.  In the case of types, this
means, as you say, substituting numbers for types, replacing
Cartesian product by multiplication, etc.., and then evaluate the
values of the two Card(type)s at various numbers.  In the case of
code, we'd just run the two different programs on the same data,
and see if we got different results.

Of course sometimes we'd like to time, or take the temperature of
the computer, for the runnings of the two programs, because there
are programs that are different, but have the same input output
behavior.

I will not post more tonight.

oo--JS.

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