Menu
▾
▴
Re: [Maxima-discuss] putting a symbol into a numeric formula, a use for a NaN?
|
From: Henry B. <hb...@pi...> - 2024-03-01 18:41:38
|
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 <ca...@ma...> Sent: Feb 29, 2024 1:04 PM To: Henry Baker <hb...@pi...>, <ca...@ma...> Cc: Stavros Macrakis <mac...@gm...>, Richard Fateman <fa...@gm...>, <max...@li...> <max...@li...> 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 > Max...@li... > https://lists.sourceforge.net/lists/listinfo/maxima-discuss > > _______________________________________________ > Maxima-discuss mailing list > Max...@li... > https://lists.sourceforge.net/lists/listinfo/maxima-discuss > -- Camm Maguire ca...@ma... ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah |
