Lambda the Ultimate

I recall that in the early 90s there were a few researchers interested in using Prolog to semi-automate the extraction of code from specifications in Z (the ancestor of B). This would fit the posters requirements, I think.

Most people using mathematics know that many constructs are not automatically computable. But, in practice, there are constructions for most of the things that one really cares about anyways. The constructions are sometimes not universal, sure, so automation is out. That's what makes it fun!

I really love (automatic) type inference. But I would be even happier with a type system which was mostly automatic and, once in a while, ``asked for help'' (not interactively). Then I would have to provide more evidence for what I am asserting to be true (assuming I am right!).

Some proof systems try quite hard to walk that pragmatic fine line -- I have the impression that that is where PVS tries to go. That is where IMPS definitely went. Coq is impressive, but I get a pre-IO-monad-Haskell kind of vibe...

In any high level language there is already a working mode that does what you require: when the computation gets stuck, raise an exception. This is also a request for help.

Since I'm thinking more shallow about this topic than most of you do, I would propose a worse-is-better strategy: drop the global consistency requirement with the axiomatic base and work with abstract interpretation as a conventional programming technique. The latter means that any programmer can write down terms like:


even a;
odd b;
c = a+4*b; // no prior value assigment to a and b necessary

and perform checks

type(c) -> even


It is only required that the type rules to determine the type of c are explicitely stated in the source code. This can be done for example using operator overloading in conventional OO languages and being performed at runtime. These rules might be quite delicate in practice ( testing set membership ) but as you said, performing delicate computations is programmers business anyway. No one really bothers that there is no Ueber-algorithm .

Proving that the type rules, stated in application code, are sound is what theorem provers are about. Instead of dropping this requirement completely it might be delayed. Of course this would induce another split within the PL language communities ( just like that of static / dynamic typing - maybe it's even the same split ) but I do think we can perfectly live with it.

Indeed PVS has a method of doing type-checking and proving simultaneously, almost hiding it from the user completely using automation (in simple examples). In Coq, this is harder because proofs are concrete objects of the calculus and manipulating them is awkward but necessary. However, we can build a PVS-like mode on top of Coq where the user do not write proof handling code and the type system infers as much as possible, leaving some proofs as obligations to be solved automatically or interactively depending if you have a decision procedure for the corresponding theory or not. This is exactly what the new Program extension of Coq does. Here's an example of using it to program quicksort.

Sir, can you make it clear to me, how your more than 100 lines of quicksort is usable in "reality", please? Show me one top-notch programmer out there (send it to Stroustroup and post his answer here, or something like that) who can from the stand understand this "monster".

I am more and more clear that I couldn't make my ideas(or better thoughts) clear to anyone here: I am in search of a very elegant solution for "real world" programming.
So one day I had these thoughts which I wanted to discuss with people who are Programming Language geeks:"Would it be a good solution to make the structures/objects of mathematics one to one directly accessible for a programmer?"

But now I see: You are in one world, I am in one world.

All you are talking about are proofs and formal methods which are really important, I know that. I am in search for a totally different thing.

I want something which small kids to financial professionals to physicians to medics to scientists can use. Easy, clear, learnable in 10 minutes (because you learned it - the basics - already in school).

Maybe you should state clearer what you expect from a type system and why did you mention type systems at all? The main purpose of a type system is to rule out certain classes of expressions as being ill typed. This makes resoning about program source code simpler, which leads among other things to compiler optimizations. So when you say that programming shall rely on set theory ( reasonable hints were given in the comments for existing implementations of modeling languages based on the Z-formalism ), one might ask why?

When you are concerned about programmers, having easy access to programming language constructs as in the tradition of modern scripting languages, why don't you drop the requirement of the foundational role of sets and type systems that are based on them, even when it's shown to you that these lead to rather arcane tools? Maybe you should work out yourself a simple prototype in Java, Ruby or any other of your favourite languages to become clear about your own motives and what is possible and what is not.

I want something which small kids to financial professionals to physicians to medics to scientists can use. Easy, clear, learnable in 10 minutes (because you learned it - the basics - already in school).

I don't think an axiomatic set theoretic approach to fundamental concepts is easily learnable in 10 minutes and necessarily suitable for physicians and financial professionals. I think you need to consider that alternative foundations approaches, such as that of topos theory, provide more programming friendly basics -- indeed and elementary topos is equivalent to a local language for a local set theory built using Martin-Lof Type theory. As others have pointed out, things like Ontic and Epigram provide a type system that fits very naturally with such a foundation. If all you really want is the gloass of mathematical feel then maybe something like Fortress would better suit you?

First of, pardon the overly polemical topic. I think too there is a gross misunderstanding here.
I linked to this certified implementation of quicksort as an example of using Coq in response to J. Carettes post, and in no way did I imply it was a response to your problem.

Now, this implementation of quicksort is 10 lines long, the proof that it is indeed doing what you want is taking the rest of the file, and I'm pretty sure you and Stroustrup could understand the meaning of the two "Program Fixpoint" definitions. The monstruosity of the proof scripts that I left in I'll have to agree too though :)
This program can be used as part of a larger development of certified software, that's how it is usable in reality.

About your question, I think what you want is a programming environment like the one I described (from "my world") because set theory simply isn't directly implementable (in "your world"), as other people pointed out. Basically the problem is that you have lots of indeterminism and non-computable objects which does not fit well with programming which is mostly giving a deterministic recipe to solve a problem. While set theory may seem so simple that every scientist know it well, it is not from the point of view of computing. There is a gap between this abstract and flexible formalism and our ways of computing. Others have already pointed out numerous systems that bridge it in one way or another.

And, as a response to my post, I quite liked what you said. For one thing, it confirmed my impression, which is always a good thing :).

There are two really under-appreciated proof systems out there: AUTOMATH and IMPS. [Yep, they are both old, and essentially dead]. PVS in some ways seems to have learned the most from IMPS. Or at least re-invented many of the same ideas. Some of the ideas in AUTOMATH (for structuring large documents) I have not seen anywhere else! Even things like Telescopes are just now being fully appreciated.

I wonder what telescopes are you talking about ? Is it the concept of typing contexts for dependent types, which is present in Coq in the form of Section variables which help parameterize a part of your development by some set of variables and definitions (a context),
or is it something else ? I couldn't find anything after (quickly) glancing at what remains of AUTOMATH on the net.

Automath archive

What I meant were explicit towers of dependent type extensions, each of whose levels could be used in proofs (and the lower the level, the simpler the proof obligations).

What you describe from Coq does sound related -- but I don't (yet!) know Coq well enough to be sure. Thanks for the pointer though.

For my next posting I am going to give you an example by implementing such a "mathematical world" into (or for the first example onto) a known PL to make it very clear what I mean.

Aldor has a large library of types built up around mathematical constructs, as you describe (it started life as the scripting/extension language for a computer algebra system). It may be of interest to you.

By the way, it's untrue to say that today's PLs don't support sets. For example, when I learnt Pascal (Borland's Turbo Pascal 5.5, ca. 15 years ago now) it had them as a built-in language construct. Language-level support for relational algebra is also emerging: see C# 3.0 for example, with it's "LINQ" technology.

Hope that helps.

Aldor is purely signature based, and even though it does have some support for dependent types, there is no type-level evaluation, so you can't have axioms as part of your type :-(. There is a variant of Aldor which can do this, but as far I know it will not get merged into the main branch. So you can't have a proper definition for a field (or even a group). Rather like Haskell, where monads are syntactic objects even though everyone treats them as semantic. Very dangerous.

This also reminds me of the OBJ family of languages which may also bear looking at.

Yes, all of those are worth a close look. The only downside is that it is very hard to figure out what kind of tool support exists for all of them. Basically they need the equivalent of a theorem-proving system as an underlying tool, and it is not clear which of them have that. Without decent tool support, most of those specification languages are, IMHO, much too complex to work with ``in the abstract'', as it were.

CafeOBJ and Maude both provide analysis/evaluation environments for OBJ-style specifications. The language associated with SpecWare is slang (or meta-slang?), but I'm not sure if there are any publicly available SpecWare tools. I'm less familiar with CASL, but alternatives like Isabelle, HOL and PVS provide excellent automated analysis support.

CASL is supported by Hets, which links up CASL specs (and other extenstions, such as HasCASL and CoCASL) to a variety of tools, including Isabelle as a theorem prover.

If you want something that natively handles groups, rings, semigroups, monoids, fields, polynomial rings, etc. as types then you probably want Magma, which provides an exceedingly rich mathematical type system.

Magma is great. And it does way more than algebra. Although as far as I can tell it does not have proper dependent types, so that it can't catch trivial errors (like adding 2 matrices with non-equal dimensions). So that's not that mathematical.

And Magma does not do analysis. Axiom does -- but it cheats, it uses an Expression type, which is well-known in type theory as a Universal type, ie a type where you can stuff in anything you want. So that's not very satisfying. Magma as, until now, avoided the issue by not trying to do any analysis (ie calculus). My spin on that is that the way humans perform calculus kinds of computations is via using an intensional rather than an extensional logic. People doing programming languages have started using modal logic(s), but not full-blown intensional logic (yet).

Guess why type-system-wizard Oleg had to resort to Template Haskell when he did his (second) version of a typed symbolic differentiator? That would be because there is no way to do it in Haskell proper. Sure, he had a rather clever first version, but that did not scale -- simplification could not be performed. When you try to mix the two, you are forced to escape from the type system. Or at least, that's the current state-of-the-art.

Expression-to-expression symbolic integration is much, much worse. And people who buy things like Maple and Mathematica and MuPAD really want integration, summation and differential equation solving (ie expression-to-expression). And, lo and behold, there are no typed systems which offer this properly (Axiom's use of the Expression ``type'' is tantamount to giving up on types, so that does not count).

The catch with calculus is that it in inextricably tied to the infinite, which, in general, computers don't necessarily handle that well. The Risch algorithm for symbolic integration, for instance, cheats by converting the problem into an algebraic one. I do wonder if an different approach, say smooth infnitesimal analysis, which has a conception of the continuum that is perhaps more amenable to computation, might be the way to go. Of course you're changing your logic to do that, and doing non-standard analysis as a result, but it might be something...

I thought I was alone in recognizing that the Risch algorithm was a cheat, since it doesn't solve the right problem! [I've talked about that in the past, there's some slides on my publications page]. In my opinion, Risch introduces more problems than it solves... although it is still an amazing scientific result.

Smooth infinitesimal analysis, in some guises, is already gaining some ground in this area: there are purely constructive versions of this theory (see the the Wikipedia page and links therein), but the category theory required is beyond me.

Except that this approach denies the existence of discontinuous functions! And, as it turns out, I rather like some kinds of discontinuous functions. So I am rather torn...

Well when you conceive of the continuum in the manner required for smooth infinitesimal analysis, which as you rightly point out, has completely constructive approaches, the fact that all functions are uniformly continuous falls out as an immediate necessity. It is a different continuum. These are, unfortunately, the trade-offs one has to make. Constructive analysis and discontinuous functions just don't mix (at least not very easily). It's really a case of "choose your poison".

The catch with calculus is that it in inextricably tied to the infinite, which, in general, computers don't necessarily handle that well.

While true that computers and infinite things don't go well together, it's not entirely true that calculus demands a continuum. It's a question of what you're trying to solve. My background is primarily computational physics, where often the fastest algorithm is one that states the problem in the most natural way for a computer. Of course, the biggest road-block is usually the demands of physical consistency.

One of the lessons that I'm still learning is that physics has less use for the real numbers and a continuum than I used to think. For example, the classical formulation of electromagnetism requires fields, which are basically point-defined quantities over all of spacetime. The formulas involve partial differentiation wrt all sorts of variables. However, all that is really obscuring what's really going on: if I have a chunk of spacetime, then the amount of "stuff" that goes in is equal to the amount of stuff that comes back out. The latter picture can be applies to a spacetime tesselated with triangles as well as just imagining arbitrary surfaces in a R^4 spacetime. I just assign to each face a number representing the flux, and can get the amount of stuff in a volume by just adding up the faces bounding a volume. There's a whole algebra available, which parallels differential geometry over continuum manifolds.

Similar things are possible with fluid dynamics, elastic materials simulations, or even general mechanics (though it gets more abstract, and not neccessarily yielding a computationally convenient view). The point is that actual analysis or vector calculus, etc. aren't actually necessary for a lot of the physics.

There's a lot of work in physics currently towards an algebraic approach to things, so that physical systems are defined by an operator algebra. Actualy computations are done by turning that algebra into a "representation" with representation theory. However, currently we can really only tackle turning groups into matrices, and even then the matricies aren't necessarily suitable for efficient computation. The biggest impediment to directly converting the operator algebra to a computational format is that no language currently allows easy and efficient quotient types.

That's all true, but it is essentially just approximations to calculus -- you are approximating the continuous space with a discrete one that allows for discrete calculation which can be performed on computer. It is the same with, for example, numerical methods to solve PDEs.

What you are talking about is the degree of precision you require in your final result. If you approximation results in smaller uncertainty/error than the required precision then yes, the approximation is just as good as the calculus. The catch, however, is that things don't always behave nicely. Numerical solutions to PDEs, for example, tend to behave nicely at the start, but the error balloons dramatically as things progress. There are a lot of problems where this doesn't cause any problems, but there are just as many problems where it make apprximation/numerical techniques useless. You can tend to get a skewed perspective on the relative frequency of the two classes because we tend to do a lot more of the former (since we can do them), and do our darndest to ignore or simplify away the latter (since if they crop up, we essentially have a roadblock).

Take for example fluid dynamics. Fluids are actually composed of millions of tiny particles. But we pretend that they're continuous, because then we can use calculus and it's more mathematically tractable. The numerical methods used to solve PDEs are actually probably closer to the real physics than the calculus that they're approximating. (I'm thinking for example of finite difference methods).

But when you discretize a PDE you are not reducing back to those untold numbers of particles, but simply approximating an approximation. Further, you also have to argue that time is discrete for other numerical methods, which is certainly an open conjecture. I don't see that you are actually getting closer to "the real physics", just finding a different gross approximation for it.

My main thrust, perhaps somewhat lost, is that calculus as we usually approach it, based on the concept of functions evaluatable at points, is not natural for describing physics. Rather, already-integrated quantities, like flux through a given surface are the natural level to see things; for example, in this case instead of a seperate field and the geometry that we consider, we only ever deal with a (formal) product of the two. This particular thread run back at least to Faraday, who described electrodynamics as "force loops", i.e. potential around a loop. More recently, we see that quantum gravity has started to take this as its departure, in particular loop quantum gravity, which posits that the fundamental observables of space are measured over loops. Now, for me, coming strictly from a point of view of computation, the finer details aren't relevant; nevertheless, naturally discrete versions of things are just easier, and usually more numerically robust, to implement.

To be more on topic: I think physics is undergoing a somewhat structural revolution, where we start focusing more on algebraic methods to describe things. Unfortunately, we currently don't have languages well suited to algebra -- algebraic identities are a pain. Personally, I think that decent, efficient quotient data types would solve a lot of things, but I have no idea on how to implement that... *grin*

Addendum: admins, please say if all this physics is inappropriate for our forum.

Personally, I think that decent, efficient quotient data types would solve a lot of things, but I have no idea on how to implement that... *grin*

I've mentioned a paper here and other places on LtU that talks about Quotient types in polymorphic programs.

Cellular automata explicitly model particles (very approximately). Finite difference methods are closely related to cellular automata. So actually, you do kind of end up back to those "untold numbers of particles".

Maybe the answer i deserve is "go study", but i find this line of comments about calculus being hard interesting, but i cannot yet grasp the reasons for that. I can imagine how infinity may have something to do with it, but i dont really get it. Or is it because you must talk about formulas to define the process of computation?

Can anyone please elaborate a bit on this and maybe give some easy pointers to read about it?

Thanks in advance.

Lucio.

Infinity is tricky. There are ways we can deal with it computationally, but it depends on exactly how it arises. The practical way to deal with infinity is to discuss the arbitrarily large. Thus we can have a Turing machine with an infinite tape, which simply means we can have an arbitrarily large position on the tape. Equally we could have a list of infinite length presuming that we only ever need to address one element at a time -- we can ask for the nth element where n is arbitrarily large and all will be fine. Infinity on an "as needed" basis works computationally because we don't need to ever actually get to infinity, just "as big as we like", and thus we can work constructively.

Things start to go off the rails when it comes to calculus however, because now we are dealing with a continuum, and our computations have infinity as a whole intrinsically bound up within them. Both differentiation and integration are the limit of some infinite process, thus "arbitrarily large" isn't good enough anymore; to actually get the answer we need to get all the way to a completed infinity, which you'll never achieve computationally.

In practice we do things like symbolic differentiation and integration by converting them into algebraic problems manipulating expressions, rather than as analysis problems dealing with functions over a continuum. Thus we end up with "expression" types as Jacques points out, rather than proper function types as one would expect.

The question that I have been struggling with for over 10 years now is: when analysis is most definitely not algebra, why are algebraic manipulations so often effective in giving answers to problems in analysis?

More precisely, given a specific problem (ie explicit formulas) and an explicit transformation to perform, often algebraic techniques work. On the whole, it seems that this works a little too well.

My current conjecture is that this has to do with 2 things: model theory and Kolmogorov Complexity. Basically, when the problem (and its answer) is small (small via KC, and model theory comes in because we were able to write it down at all!), then there is so much rigidity around that the difficult analytic problem is nevertheless appropriately captured by algebra.

Contrast the following:
1) in Type 2 theory of constructive functions, all functions are continuous, but differentiation is uncomputable.
2) using ``expressions'' to represent functions, differentiation is trivial (an easily written term-rewrite system).
The thing is that view #1 represents functions via approximations, and so builds-in a strong sense of the infinite -- not strong enough to lose continuity, but strong enough to lose differentiation. View #2 allows you to write down some nonsense functions, but since most of the basic building blocks are analytic, you tend to end up with differentiable results (unless you get complete nonsense).

My current favourite expression is 1/(1/(x-x)). Most computer algebra systems believe this is the constant 0. Many compilers do too. Of course, strict operational semantics give _|_ everywhere.

My second favourite is probably (x-sqrt(x^2))*(x+sqrt(x^2)), which shows that ``expressions'', even rather simple ones which represent total functions, contain zero-divisors (when interpreted operationally), so do not form a nice algebraic structure at all.

Perhaps something like Kanren would be interesting to you. It really does seem to me, perhaps naïvely, that you want Kanren or Ontic.

Logical languages let you speak of "relations". In fact, often logic languages (e.g. Prolog) or similar things are used/desired for query languages (as opposed to SQL). As one example, Escher a functional logic language has interesting support for sets.