FOM: Re: Midwest Model Theory Meeting

[Charles Silver]

Andrej Bauer writes:

>TO CHARLIE SILVER:
>
>On  8 Nov, Charles Silver wrote:
>> Vaughan Pratt:
>>>The inventor of Boolean logic also invented the finite difference
calculus
>>>("A Treatise on the Calculus of Finite Differences", first edition 1860,
>>>second edition substantially reworked by John Moulton 1872), whose
toolkit
>>>provides induction-free methods for a much larger class of such problems,
>>>including summing n^i for fixed integer i and much more.
>>
>>
>>     Can these methods be formalized?
>>
>
>Yes, there are algorithms that find closed-from solutions of summations.
>The most famous one is Gosper's algorithm that finds a hypergeometric
>closed form of an indefinite hypergeometric sum. This was generalized
>by Zeilberger and Wilf, and Petkovsek. See the book "A = B" by these
>authors, at
>
>http://www.cis.upenn.edu/~wilf/AeqB.html
>
>where you can get a pdf version of the book and Mathematica and Maple
>implementations of the algorithms. All of these algorithms are much more
>general than the difference method. They work by translating a summation
>problem S[k] = Sum[t[k], k] to a difference equation
>S[k+1] - S[k] = t[k] and proceed from there.
>
>The latest in this area is a generalization of Gosper's algorithm by
>Petkovsek and myself to "mixed multibasic hypergeometric series",
>whatever that means. We have an algorithm, but we do not have any
>real-world problems to apply it to! So, if you know of any problems
>where you try to sum something of the form
>
>   Sum[t[k], k]
>
>where t[k+1]/t[k] = R[k, q_1^k, ..., q_m^k], where R is a rational
>function in its arguments, and q_1, ..., q_m are constants, please tell
>me. For example, it could be something crazy like
>
>  t[k] = (2^k + 3^k) / (k! * 5^(k^2 + 1)).


    Thank you for explaining this to me.  I responded overly quickly to
Harvey's message, not realizing that the point of John Baldwin's and Harvey
Friedman's question was to arrive at a formalization of this kind of
reasoning.   I want to respond to Vaughan Pratt's message in a similar way,
so look for a continuation of this message in my reply to him.  Thanks
again.

Charlie Silver