[konjin]

I find it odd that you pretend a meta-mathematical question is a mathematical one.

You are dismissing constructivism as not mathematics, and you ignore that the halting problem is a way to deal with a class of results which include non-existence proofs by running an algorithm forever.

I can easily create calculations that will never return results which classical mathematics say are impossible by the simple fact they never return any results at all.

The Risch algorithm being a complex example, finding the square root of two in the rational number domain being a simple one. I can still deal with them as though they return results in all calculations though, without the need for baroque semi-mystical notation. Unless you want to claim some sort of divine human essence not present in Turing Machines and Lambda Calculus which lets us transcend their computational capabilities?

[Tainnor]

I literally don't understand what the hell you are talking about.

But this has nothing to do with constructivism. Even if you only allow constructive definitions and proofs, there is still the world of a difference between the definition of an integral and the result you get from evaluating it.

Yeah, sure, in theory you can represent an integral as a function that takes another function and two boundary points and returns a value...

But first, it may not be possible to determine the value of the integral exactly because there is no known method of doing so (the Risch algorithm, apart from it basically being so complex that it's implemented almost nowhere fully, only works for elementary functions!).

And second, if integrals are "just functions", you lose the ability to manipulate them according to known theorems, e.g. additivity, triangle inequality, Cauchy-Schwarz, convergence theorems, ...

So yeah, here's where I get the feeling that some people should do some more maths and spend good parts of their days proving theorems and playing with definitions before they start complaining about how dumb its language is.

[konjin]

>So yeah, here's where I get the feeling that some people should do some more maths and spend good parts of their days proving theorems and playing with definitions before they start complaining about how dumb its language is.

Some people have a PhD in mathematical physics and wrote the higher function code of axiom. I guess those people would be difficult to understand for non-experts.

[Tainnor]

Ok, I misjudged your experience apparently, but you could still do a better job actually engaging with the arguments.

[konjin]

You sound like a third year maths student who has just been taught the Lebesgue integral and has decided that it is the _real_ definition of definite integration. Quite frankly I don't have the energy or inclination to have adversarial arguments with people who don't understand what I'm saying. Maybe talk to your professors about the generalizations of integration and why none of them are the 'real' way to integrate a function.

Also the integral procedure defined at the top isn't a function, it's an operator. It returns functions as results, not values.

[afiori]

I don't know lisp so maybe there where more nuances in your code, but often your want to analyse an integral in symbolic terms (for whatever integration definition you are using)

The expression of the integral operator as a function in code is contrary to that with how people usually think about functions and code.

The only language I know that properly manages to represent integrals as code is Wolfram Mathematica by using rich rewrite systems.

That is Integrate(f,a,b) is not code but a data structure to be interpreted by an external (and customizable) integration context that defines numerical types, algorithms, lazyness, etc.

From the links I know of Wolfram Mathematica and lisp this could well be what you meant, but it is quite different from giving a single integration algorithm.

[Tainnor]

Many (if not all?) CAS have some internal tree representation of mathematical structures, Mathematica is not the only one. I worked on such a system myself. To define data types for your expressions and then evaluate them via different algorithms is quite natural. So yes, we also used something like Integral(f, from: a, to: b) and then had like a gazillion techniques to actually evaluate that.

Proof assistants do something similar btw, they also encode mathematical expressions as (often recursive) data types and then prove things about those definitions.

edit: to be fair though, the LISP implementation proposed to use the Risch algorithm, which actually does give you symbolic antiderivatives. So that wouldn't be a valid critique of the implementation. There more salient points are a) that the Risch algorithm only works for a certain class of functions (those that have an elementary antiderivative) and b) that by not separating the definition of an integral from its evaluation, you're not able to manipulate it directly as an expression or to evaluate it via different methods (e.g. symbolic vs. numerical methods).

Just think about inputting $complicatedIntegral - $complicatedIntegral. This is clearly zero, but if your integral is "just a function", you're not able to see that and will spend an unreasonable amount of time computing it (twice, even), or worse, will fail to produce a result.