FOM: Re: Midwest Model Theory Meeting
silver_1 at mindspring.com
Tue Nov 9 12:52:45 EST 1999
Andrej Bauer writes:
>TO CHARLIE SILVER:
>On 8 Nov, Charles Silver wrote:
>> Vaughan Pratt:
>>>The inventor of Boolean logic also invented the finite difference
>>>("A Treatise on the Calculus of Finite Differences", first edition 1860,
>>>second edition substantially reworked by John Moulton 1872), whose
>>>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
>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
More information about the FOM