Re: [Maxima-discuss] putting a symbol into a numeric formula, a use for a NaN?

[Camm Maguire]

Greetings, and thank you so much for the very helpful outlines and
pointers.  Just for reference, I am a physicist, not a trained computer
scientist, and have only enough exposure to these ideas as I've gleaned
via osmosis in maintaining GCL over the years.

It does seem like there is a decades long history/evolution/battle going
on here in programming languages that may provide useful insights for a
common lisp compiler.  The basic idea of deriving a set of static
equations instead of 'symbolically executing the program' is surely
better.  It does appear that non-linearities and exponential time
decideability can occur.  The classic examples using ML assuming both
branches of an 'if return the same type are clearly useless in lisp.
And at least what I have skimmed thus far from the web, it is not clear
to me how one of the most important inferences fit into HM, that of
infering types *locally* to a given branch of an 'if given the form of
the boolean test (e.g (if (car x) (listp x) t) -> t).  There must be
some way of handling this other than doubling the type variables for
each real variable and for each 'if encountered.

There are people who have already tackled this, but it is not clear that
some variant of the HM engine has made its way into any production
common lisp system.  If anyone knows for sure that would be helpful.
And if not, if anyone knows why not, that would also be helpful.

It also seems part of the accepted common lore that lisp is somehow more
primitive or deficient in this regard and is to be abandoned in favor of
more modern languages like ML, Haskell, .... And indeed in many lisp
projects, the first thing they do is define their own language on top of
lisp.  I wonder what the substance is here or if this is just a matter
of personal taste.  I do understand that if a language's compilers
cannot deliver equivalent performance to another, that is eventually a
fatal flaw.

Take care,

Henry Baker <hbaker1@pipeline.com> writes:

> Re type inferencing for Common Lisp:
>
>  
>
> Hi Camm:
>
>  
>
> As you no doubt know, some of the most sophisticated type inferencing
>
> systems in use today are the Hindley-Milner style inferencers, used
>
> in a number of 'functional programming' languages and an enhanced
>
> version is used in the Rust programming language.
>
>  
>
> https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system
>
>  
>
> Hindley-Milner type systems build up a set of equations, which can
>
> be solved for the actual type.  Once the set of equations have been
>
> derived, there is no more 'forwards' or 'backwards' inferencing,
>
> because we're solving for a *static* solution which works in both
>
> directions.
>
>  
>
> As you know, the traditional Lisp systems provided for a relatively
>
> obvious *forward* inferencing, which is basically a symbolic execution
>
> of the program in the forward direction.
>
>  
>
> It is also possible to do a similar *backwards* inference by doing a
>
> symbolic execution of the program in the reverse direction.  Except
>
> for very special programs, a typical backwards inference -- by itself --
>
> won't produce very tight range bounds.
>
>  
>
> It is also possible to do both forwards and backwards inference -- e.g.,
>
> forwards from the parameters of a function to its result type, and backwards
>
> from its result type to the parameters of the function.  Depending upon the
>
> type lattice chosen, such forwards & backwards inferencing process may never
>
> converge -- e.g., producing tighter and tighter bounds, but never a final
>
> static bound.
>
>  
>
> If a symbolic mathematical system -- e.g., Maxima -- were available, it would
>
> be possible to create type bounds with *symbolic variable parameters* and
>
> create a set of simultaneous equations using those variables, which could then
>
> be solved for final *static* bounds.
>
>  
>
> Indeed, a number of modern compilers do a quite nice job with the variables
>
> involved in *index arithmetic*, so that the vast majority of bounds checks
>
> in tight loops can be eliminated.
>
>  
>
> As you might imagine, solving some of the equations generated from such type
>
> bounds simultaneous equations might involve some fairly deep mathematics -- 
> e.g.,
>
> proving from first principles that a series for the sin(x) function will 
> always
>
> fall into the range [-1.0 .. +1.0].  So the knowledge required for such bounds
>
> inferencing will need to be arbitrarily sophisticated.
>
>  
>
> A comment on 'assert':
>
>  
>
> A good compiler will notice that 'assert' fails when its predicate argument
>
> evaluates to false at run-time.  Thus, the addumed truth of this predicate
>
> can be utilized later during forwards inferencing, or earlier during backwards
>
> inferencing.  Thus, an 'assert' can be used as a *hint* to the compiler about
>
> how to handle the induction involved when inferencing processes a loop or a
>
> recursion.
>
>  
>
> One overall goal of the compiler is to convert 'assert' predicates into 
> compile
>
> time *constants* -- i.e., provably true or false at compile time.
>
>  
>
> Some modern compiler/loader systems -- e.g., Clang/LLVM -- can continue 
> optimizing
>
> even at link/load time, when more specific information is available about the
>
> actual values of the parameters which might be encountered at runtime.
>
>  
>
> -----Original Message-----
> From: Camm Maguire <camm@maguirefamily.org>
> Sent: Feb 29, 2024 1:04 PM
> To: Henry Baker <hbaker1@pipeline.com>, <camm@maguirefamily.org>
> Cc: Stavros Macrakis <macrakis@gmail.com>, Richard Fateman 
> <fateman@gmail.com>, <maxima-discuss@lists.sourceforge.net> 
> <maxima-discuss@lists.sourceforge.net>
> Subject: Re: [Maxima-discuss] putting a symbol into a numeric formula, a use 
> for a NaN?
>
>  
>
> Greetings!
>
>  
>
> Henry Baker writes:
>
>  
>
>> Re symbols/NaNs:
>
>  
>
>  
>
>  
>
>> A long time ago, I was attempting to derive Lisp-style
>
>>
>
>> bounds declarations at compile time using 'forward' and
>
>>
>
>> 'backward' type inferencing.
>
>>
>
>  
>
> Indeed, GCL at the moment is making some pretty heavy use of bounds
>
> inferencing/propagation. It seems the most efficient way to do this to
>
> me is to define the common bounds as bits in a predefined type vector,
>
> and indeed to use floats to avoid the worst in ratios for corner cases.
>
>  
>
> One thing I would like to improve is 'backward' type inferencing, so I
>
> am intrigued by your comment. Once one establishes a binding and later
>
> figures out it must have a more restricted type than originally thought,
>
> the straightforward compiler algorithm is to iterate or throw back to
>
> the binding establishment and proceed again with the updated
>
> information. We do this in a few places such as when processing tags in
>
> tagbodies, but the general idea seems horribly inefficient in terms of
>
> compiler speed. What is the best way to collect 'backward' type
>
> inferencing while processing code as few times as possible?
>
>  
>
> Take care,
>
>  
>
>>
>
>>
>
>> For the heck of it, I tried my type inferencer out on a
>
>>
>
>> Newton sqrt iteration, and it dutifully tried to do the
>
>>
>
>> computation at compile time, except using Lisp-style 'bounds'
>
>>
>
>> as a data type. Since the Lisp standard requires *rationals*
>
>>
>
>> for declaring numeric bounds, I quickly got bounds with enormous
>
>>
>
>> denominators.
>
>>
>
>>
>
>>
>
>> I never tried using range arithmetic with floating point bounds
>
>>
>
>> as approximations to the rational bounds, but perhaps that might
>
>>
>
>> be the *best* use for FP range arithmetic in Lisp ! So long as
>
>>
>
>> the FP bounds are *always* looser than the rational bounds, then
>
>>
>
>> the FP bounds should still be useful, and the FP type inference
>
>>
>
>> calculations will be far more efficient than the rational type
>
>>
>
>> inference calculations were.
>
>>
>
>>
>
>>
>
>> BTW, I also worked out a system using Henrici *circular arithmetic*
>
>>
>
>> for implementing continued fractions for sqrt's; perhaps not the
>
>>
>
>> fastest way to compute sqrt approximations, but maybe the most
>
>>
>
>> elegant?
>
>>
>
>>
>
>>
>
>> -----Original Message-----
>
>> From: Stavros Macrakis
>
>> Sent: Feb 29, 2024 11:30 AM
>
>> To: Richard Fateman
>
>> Cc:
>
>> Subject: Re: [Maxima-discuss] putting a symbol into a numeric formula, a use 
>> for a NaN?
>
>>
>
>  
>
>  
>
>> Won't the Newton iteration typically be wrapped in a while clause? How will 
>> the termination condition be evaluated?
>
>>
>
>> On Thu, Feb 29, 2024 at 12:32 AM Richard Fateman wrote:
>
>>
>
>> In the context of taking a numerical program and reusing it
>
>> with partial symbolic input, here's another example..
>
>>
>
>> Here is one step of a newton iteration: x[n+1] = x[n] - f(x[n])/df(x[n])...
>
>>
>
>> newtstep(f,x,val):= block([d:diff(f,x)], val- subst(val, x,f/d));
>
>>
>
>> how does this work? val is a guess... here, a guess the root of x^2-9...
>
>>
>
>> newtstep(x^2-9,x, 5.0); --> returns 3.4
>
>> newtstep(x^2-9,x, 3.4); --> returns 3.023529411764706
>
>> newtstep(x^2-9,x, 3.023529411764706); --> returns 3.00009155413138
>
>> you get the idea.
>
>>
>
>> Now try putting an expression in there for the guess.. [ could use a NaN 
>> perhaps]
>
>> newtstep(x^2-9,x,3-eps)$ /* could put 5-eps or anything else...
>
>> newtstep(x^2-9,x,%)$
>
>> newtstep(x^2-9,x,%)$ -->
>
>> -((eps^8-24*eps^7+504*eps^6-6048*eps^5+45360*eps^4-217728*eps^3+653184*eps^2-1119744*eps+839808)/(8*eps^7-168*eps^6+2016*eps^5-15120*eps^4+72576*eps^3-217728*eps^2+373248*eps-279936))
>
>>
>
>> whew! try to understand this by using Taylor expansion..
>
>>
>
>> taylor(%,eps,0, 9) --> 3+eps^8/279936+eps^9/209952
>
>>
>
>> The newtstep program could instead be some large mysterious
>
>> iterative numerical program in a language that normally does not
>
>> allow symbols. But we might fool it by using NaNs as substitutes for symbolic
>
>> expressions.
>
>> If you had this all hooked up via trap handling
>
>> you might get some insight as to how a program works..
>
>>
>
>> RJF
>
>>
>
>>
>
>> _______________________________________________
>
>> Maxima-discuss mailing list
>
>> Maxima-discuss@lists.sourceforge.net
>
>> https://lists.sourceforge.net/lists/listinfo/maxima-discuss
>
>>
>
>> _______________________________________________
>
>> Maxima-discuss mailing list
>
>> Maxima-discuss@lists.sourceforge.net
>
>> https://lists.sourceforge.net/lists/listinfo/maxima-discuss
>
>>
>
>  
>
> --
>
> Camm Maguire camm@maguirefamily.org
>
> ==========================================================================
>
> "The earth is but one country, and mankind its citizens." -- Baha'u'llah
>

-- 
Camm Maguire                                        camm@maguirefamily.org
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah