You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Following some recent discussions on Slack, I'm considering writing a HOL conversion for computing indefinite integrals (antiderivatives) of real functions, which may be called INTEGRATE_CONV.
After some investigations on the underlying algorithms used by CAS software, I found a direct porting of these algorithm into HOL (as ML functions, with intermediate values as HOL theorems) is infeasible: not only these algorithms are extremely complex but also sometime they requires theories beyond HOL's current status.
A feasible approach which can be implemented in relatively short time is to use CAS software as external oracles. For an input function f(x), the CAS software will return another function F(x). Then, on the HOL side, all we need to do is to verify if D(F) - f = 0 is true, and this can be done by simplifying D(F) - f using existing conversions provided by realLib. If transcendental functions are involved and the existing simplifier is too weak, we can improve the simplifier.
(Note that the existing Diff.DIFF_CONV does not do any simplifications on its outputs. But users of DIFF_CONV should have been used to further simplify the outputs on their own.)
If we use the following FTC theorem as the working basis:
[FUNDAMENTAL_THEOREM_OF_CALCULUS] Theorem
⊢ ∀f f' a b.
a ≤ b ∧
(∀x. x ∈ interval [(a,b)] ⇒
(f has_vector_derivative f' x)
(at x within interval [(a,b)])) ⇒
(f' has_integral f b − f a) (interval [(a,b)])
Let f be the input function and F be the desired antiderivative (from external oracle), a call of INTEGRATE_CONV ``\x. f`` should output a theorem like this:
⊢ ∀a b.
a ≤ b ∧ (∀x. x ∈ interval [(a,b)] ⇒
(f has_integral F b − F a) (interval [(a,b)])
or just (maybe)
⊢ ∀x. (F has_vector_derivative f x) (at x)
Below I describe how a CAS software called "Axiom" [1] is used as an external oracle. This software is quite strong in doing symbolic integration as it implements a decision procedure: for any so-called "elementary function" (NOTE: all transcendental functions are elementary), if the software cannot give the result, then it means the antiderivative function does NOT exist in finite form.
To use Axiom as an oracle from HOL, on HOL side the input function should be written into a temporarily file, then Axiom command is called, then the output is expected in another temporarily file, in an acceptable format.
For example, once Axiom is installed, I can put the following file as my $HOME/.axiom.input: (which comes from Axiom distribution)
--Copyright The Numerical Algorithms Group Limited 1994.
-- This file is read on start-up by the AXIOM system. It is
-- most commonly used to customize the user's environment via the
-- )set system commands.
-- do not enter lisp break on error
)set break nobreak
-- use the simple character set
)set output char plain
-- everyone uses this
)set userlevel development
-- make the highlighting characters go away
)set message high off
)set message prompt frame
-- read the user's synonym file for system commands, if it exists
)read "mysyns.input" )ifthere )quiet
The idea is that, Axiom will try to read mysyns.input in current directory as the input, if exists. Suppose the input function is x pow 2, on HOL side this function should be converted into Axiom's format, x ^ 2 or x ** 2, and be written into a file mysyns.input together with other Axiom commands:
)set output algebra off
)set output fortran on
)set output fortran output
)set fortran optlevel 0
)set fortran segment off
)set fortran ints2floats off
)set fortran precision single
)set quit unprotected
)set message type off
integrate(x^2,x)
)quit
The commands in the above file set the output format to FORTRAN and output target to a file named output.sfort (the part .sfort is added by Axiom), and then call the integrate function on the input function. If I start Axiom in the same directory, with the following command:
$ axiom -noht -nogr -noclef -nox
I will see the following outputs on screen, which indicates that the result has been written into output.sfort:
AXIOM Computer Algebra System
Version: Axiom (May 2017)
Timestamp: Thursday June 30, 2022 at 10:59:57
-----------------------------------------------------------------------------
Issue )copyright to view copyright notices.
Issue )summary for a summary of useful system commands.
Issue )quit to leave AXIOM and return to shell.
Visit http://axiom-developer.org for more information
-----------------------------------------------------------------------------
Re-reading interp.daase
Re-reading operation.daase
Re-reading category.daase
Re-reading browse.daase
FORTRAN output will be written to file
/Users/binghe/Lisp/axiom/output.sfort.
The contents of output.sfort is this: (note that there are six whitespaces before R1, this whole file is a valid FORTRAN (77?) program)
R1=(1/3)*x**3
For a more complicated input function like tan(atan(x)/3), the output is the following: (note that the 2nd line continues the 1st line by having & after five whitespaces. This seems also FORTRAN-derived.)
At this step, either the FORTRAN-compatible expressions are parsed by some ML code to be converted to HOL terms, or at Axiom side we can inject some user library code to output function expressions in HOL's directly acceptable format.
Of course, another open source CAS software can be used instead, e.g. Maxima (what else could be here?). But from the above notes I guess there's no easy way to support a wide range of different CAS software because each of them has different input/output formats.
Nasser wrote:
>
> newbie here.
> I can't figure how to tell fricas to output result of command in 1D plain
> text, instead of the default 2D.
>
> I tried all combinations of the )set output commands, but nothing is
> working for me. All I want, is that instead of
>
> integrate(sin(x)*cos(x),x)
>
> 2
> cos(x)
> - -----------
> 2
>
> is to get
>
>
> - cos(x)^2/2
>
> Spend 30 minutes, reading docs, googling, and I can't find one example how
> to do this. Closest I found is
>
> (7) -> )set output algebra off
> (7) -> )set output fortran on
> (7) -> integrate(sin(x)*cos(x),x)
>
> R7=-DCOS(x)**2/2
>
> But I do not want fortran format. I just want 1D format instead of 2D for
> standard algebra.
>
> Please show me the complete commands to use, as I am very new to axiom and
> fricas
> and assume I know nothing about the system.
Unfortunately, normal output routines always produce 2D output.
Linear output can be obtained via 'unparse':
(1) -> ii := integrate(sin(x)*cos(x),x)
2
cos(x)
(1) - -------
2
Type: Union(Expression(Integer),...)
(2) -> unparse(ii::InputForm)
(2) "((-1)*cos(x)^2)/2"
Type: String
(3) -> ((-1)*cos(x)^2)/2
2
cos(x)
(3) - -------
2
Type: Expression(Integer)
Note: result of 'unparse' when given back to FriCAS is supposed
to produce orignal value. To make sure that result can be
parsed correctly 'unparse' may add extra parenthesis (sometimes
unnecessary).
--
Waldek Hebisch
Following some recent discussions on Slack, I'm considering writing a HOL conversion for computing indefinite integrals (antiderivatives) of real functions, which may be called
INTEGRATE_CONV
.After some investigations on the underlying algorithms used by CAS software, I found a direct porting of these algorithm into HOL (as ML functions, with intermediate values as HOL theorems) is infeasible: not only these algorithms are extremely complex but also sometime they requires theories beyond HOL's current status.
A feasible approach which can be implemented in relatively short time is to use CAS software as external oracles. For an input function
f(x)
, the CAS software will return another functionF(x)
. Then, on the HOL side, all we need to do is to verify ifD(F) - f = 0
is true, and this can be done by simplifyingD(F) - f
using existing conversions provided byrealLib
. If transcendental functions are involved and the existing simplifier is too weak, we can improve the simplifier.(Note that the existing
Diff.DIFF_CONV
does not do any simplifications on its outputs. But users ofDIFF_CONV
should have been used to further simplify the outputs on their own.)If we use the following FTC theorem as the working basis:
Let
f
be the input function andF
be the desired antiderivative (from external oracle), a call ofINTEGRATE_CONV ``\x. f``
should output a theorem like this:or just (maybe)
Below I describe how a CAS software called "Axiom" [1] is used as an external oracle. This software is quite strong in doing symbolic integration as it implements a decision procedure: for any so-called "elementary function" (NOTE: all transcendental functions are elementary), if the software cannot give the result, then it means the antiderivative function does NOT exist in finite form.
To use Axiom as an oracle from HOL, on HOL side the input function should be written into a temporarily file, then Axiom command is called, then the output is expected in another temporarily file, in an acceptable format.
For example, once Axiom is installed, I can put the following file as my
$HOME/.axiom.input
: (which comes from Axiom distribution)The idea is that, Axiom will try to read
mysyns.input
in current directory as the input, if exists. Suppose the input function isx pow 2
, on HOL side this function should be converted into Axiom's format,x ^ 2
orx ** 2
, and be written into a filemysyns.input
together with other Axiom commands:The commands in the above file set the output format to FORTRAN and output target to a file named
output.sfort
(the part.sfort
is added by Axiom), and then call theintegrate
function on the input function. If I start Axiom in the same directory, with the following command:I will see the following outputs on screen, which indicates that the result has been written into
output.sfort
:The contents of
output.sfort
is this: (note that there are six whitespaces beforeR1
, this whole file is a valid FORTRAN (77?) program)For a more complicated input function like
tan(atan(x)/3)
, the output is the following: (note that the 2nd line continues the 1st line by having&
after five whitespaces. This seems also FORTRAN-derived.)which means
At this step, either the FORTRAN-compatible expressions are parsed by some ML code to be converted to HOL terms, or at Axiom side we can inject some user library code to output function expressions in HOL's directly acceptable format.
Of course, another open source CAS software can be used instead, e.g. Maxima (what else could be here?). But from the above notes I guess there's no easy way to support a wide range of different CAS software because each of them has different input/output formats.
[1] http://www.axiom-developer.org
The text was updated successfully, but these errors were encountered: