Formal methods are not human one

[Christophe Bal]

Hello.

I'm looking for formal outputs that are not calculated as a human can do (this is for a free french "book"). Do you know such kind of examples ?

Christophe BAL

PS : this questions has been posted on both Sage and Sympy lists.

[Simon King]

Hi Christophe,

["Followup-To:" nach gmane.comp.mathematics.sage.support gesetzt.]

On 2014-10-29, Christophe Bal <proj...@gmail.com> wrote:
> I'm looking for formal outputs that are not calculated as a human can do
> (this is for a free french "book"). Do you know such kind of examples ?

I don't understand your question. What do you mean by "formal output"?
And what do you mean by "not calculated as a human can do"? I recall an
analytic number theorist who would stare at an integral filling a whole
page, and then correctly telling its value. But certainly a computer
would compute the same integral in a totally different way.

Best regards,
Simon

[john_perry_usm]

I'm looking for formal outputs that are not calculated as a human can do (this is for a free french "book"). Do you know such kind of examples ?

Like Simon, I'm no sure if this is what you mean, but Bruno Buchberger was for a while working on a proof-generating system called Theorema, and he used to show "human-readable" proofs it generated for common theorem(s) (not sure about the plural, but there was at least one) which he could not find elsewhere in the literature. You might want to look up that work of his.

john perry

[Aaron Meurer]

The most canonical example of this is symbolic integration. The two
most powerful algorithms implemented in SymPy, Risch and Meijer G,
work completely differently from how a human would compute an integral
(there are also some table lookup algorithms and manualintegrate which
do work how a human would). Risch works by converting the expression
to a tower of differential extensions (roughly, it converts the
integrand into a rational function where the variables have a
derivative which can be expressed in terms of the other variables). It
then performs what basically amounts to several polynomial
manipulation algorithms on this to compute the integral. To imagine
the difference, consider how many times you compute a polynomial gcd
(the Euclidean algorithm) as part of computing an indefinite integral
by hand. It's probably zero. By contrast, the Risch algorithm computes
gcds hundreds of times over the course of calculating an integral.

The Meijer G algorithm works (very roughly) by converting the integral
into a Meijer G function, integrating it, and then converting it back.

The usual by-hand integration methods are sort of heuristics. There
are several methods which apply to specific expressions, and if you
can pattern match your expression to a known technique then you can
apply it. Risch and the Meijer G algorithm are quite general (Risch is
extremely general, to the point where if it can't compute an integral
for an elementary function then it is a proof that none exists).

There are other good examples from the polys module. For instance, the
algorithm to factorize polynomials (again here, a human "algorithm"
would be heuristics, which might not always apply, whereas the
computer algorithm is based on some deeper math that lets you always
compute the factorization for any polynomial).

In general, I would say that human methods tend to use a lot of little
tricks, which are designed to minimize brute calculation. This is
because humans are bad at brute calculation, but very good at the
pattern matching and intuition required to apply and invent such
methods. Computers on the other hand are very good at brute
calculation, but very bad at pattern matching and intuition.

So even algorithms that are essentially done the same way by a human
and a computer are somewhat different for actual computation because
humans know when they can "skip" certain steps, for instance. A human
isn't going to run through the full Euclidean algorithm to compute
gcd(1, x), for instance, and even for gcd(x, x**2 + x) a human can see
the answer right away without running through any polynomial long
division.

Aaron Meurer

> --
> You received this message because you are subscribed to the Google Groups
> "sympy" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to sympy+un...@googlegroups.com.
> To post to this group, send email to sy...@googlegroups.com.
> Visit this group at http://groups.google.com/group/sympy.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/sympy/CAAb4jGkNc8QcUAxhYnhoRN017tEXfDZrtABVr4w_OTQEhfXSqQ%40mail.gmail.com.
> For more options, visit https://groups.google.com/d/optout.