Lambda the Ultimate

For whatever reason, I can't help but continually muse over the myriad unfulfilled promises generated by the software engineering, research and development communities over the past few decades plus, the duration of my own involvement.

Coming out of Boston in the mid-to-late '80's, there's a veritable laundry list of AI and then OOP associated promises of software heaven as yet unfulfilled. I think of the "formal methodologies" craze going back to the early 70's and my father's day up through, say, the earlier part of this decade. (While I do anachronistically find Jackson's now "outdated" books still full of well written problem solving wisdom, I don't see so many flowcharts, or object hierarchy, or object state or data flow diagrams these days.) And on a very related note, whatever became of the relatively bright promise of software construction via specification, and (IMHO) relatively lovely specification notations such as Z?

Whatever came of Gelertner's vision of massive, distributed tuple spaces, (or Jini for that matter) fronted by advanced data visualization on every desktop? Where are our catalogs, commercial or otherwise, of plugable "software components?" Why is "SETI at Home," of all the possible application domains, still probably the best known and most widely disseminated example of massively distributed computing (if I have my terminology right)?

And on and on .... So I'm very curious. What are the unfulfilled software technology promises most noteworthy to LTU members? And just as important, which of these were but ill conceived pipe dreams? But at the same time, which of these promises of yore might still warrant fulfillment with further time, effort and research?

Scott

Given the recent posts on computation and logic, those of you who will be in Silicon Valley on Thursday Jan. 7 might be interested in the following event at 4PM at SRI:

Direct Inference in Direct Logic(TM)
Carl Hewitt

Direct inference is reasoning that requires a more direct inferential connection between premises and conclusions than classical logic.

For example, in classical logic, (not WeekdayAt5PM) can be inferred from the premises (not TrafficJam) and (WeekdayAt5PM infers TrafficJam). However, direct inference does not sanction concluding (not WeekdayAt5PM) because it might be that there is no traffic jam but it undesirable to infer (not WeekdayAt5PM). The same issue affects probabilistic (fuzzy logic) systems. Suppose (as above) the probability of TrafficJam is 0 and the probability of (TrafficJam given WeekdayAt5PM) is 1. Then the probability of WeekdayAt5PM is 0. Varying the probability of TrafficJam doesn’t change the principle involved because the probability of WeekdayAt5PM will always be less than or equal to the probability of TrafficJam.

Direct inference is the foundation of reasoning in the logical system Direct Logic. Direct Logic has an important advantage over classical logic in that it provides greater safety in reasoning using inconsistent information. This advantage is important because information about the data, code, specifications, and test cases of cloud computing systems is invariable inconsistent and there is no effective way to find the inconsistencies.

Direct Logic has important advantages over previous proposals (e.g. Relevance Logic) to more directly connect antecedents to consequences in reasoning. These advantages include using natural deduction reasoning, preserving the standard Boolean equivalences (double negation, De Morgan, etc.), and having an intuitive deduction theorem that connects logical implication with inference. Direct Logic preserves as much of classical logic as possible given that it is based on direct inference. The recursive decidability of inference for Boolean Direct Logic will be proved where a Boolean proposition uses only the connectives for conjunction, disjunction, implication, and negation. In this way Direct Logic differs from Relevance Logic because Boolean Relevance Logic is recursively undecidable

To add to Ehud's proposed Clojure department: A recent Reddit thread mentioned the release of Clojure 1.1 RC 1, which features, among other things, support for ‘chunked sequences’—essentially, lazy sequences where elements are evaluated in chunks of 32, rather than on-demand. (If the behaviour sounds familiar, it's apparently what lazy bytestrings already do in Haskell.)

As a mathematician, there are few things more dear to me than laziness—of the physical sort, at least, which is perhaps why the programming sort appeals so much to me. I lamented its demise, and Rich Hickey responded with some very nice background and explanation.

This is the calculus introduced in the "Safe Type-level Abstractions in Scala" paper, and also used in "Generics of a Higher Kind." When I read the latter paper I saw something confusing, and just today I re-read the earlier paper to confirm that it contains the same thing.

In the rules for type expansion (Figure 7 in the paper I linked above), in the X_SEL case, one of the premises is (excuse my attempt to format this with ASCII):

Gamma |- [x -> T]S << R

From what I understand, x is a term-level variable, and T is a type. How can that substitution work, then? Wouldn't the result be syntactically invalid?

I wouldn't be surprised if I am missing some detail in the paper, so if anybody with a better understanding could point me in the right direction, I'd appreciate it.

Edit:
Thinking about it a bit, it seems like the premise ought to be, instead:

Gamma, x : T |- S << R

Question

What,if anything, prevents the execution of a Haskell term from being a proof in equational logic?

Below are some things thay may impede treating Haskell as a logical system with terms being true equations. Any feedback on these reasons would be welcome. Are they are valid reasons? What is their possible impact? Are there more reason?

--------------------Reason (1)------------------

There are some equations that are not expressible in Haskell e.g. mirror (mirror x) = x . It is not possible at the value level, because Haskell does not support dependent types and thus cannot express the type of the proposition "forall a . forall x:Tree a, mirror (mirror x) = x", and therefore a proof term also cannot be constructed. Another example from Torrini et al discusses specifying order. A partial order that is also linear is called a total order. The class linorder of total orders is specified using the usual total order axioms. They conclude that such axiomatizations are not possible in Haskell.

--------------------Reason (2)------------------

According to Thompson the equations in Miranda (and I assume Haskell) are not pure mathematical equations due to *where* and other reasons. According to Danielsson the fact that they are not always structurally equations does not prevent functional programmers from
using them as if they were valid equations. Danielsson show that this informal *fast and loose* use of equational axioms and theorems is *morally correct*. In particular, it is impossible to transform a terminating program into a looping one. These results justify the informal reasoning that functional programmers use.

Kieburtz states that neither the syntax nor type system discriminate between values and latent computations.
To prove some property of a Haskell program the verification logic must support such distinctions. To address this shortcomming of Haskell Kieburtz has included P-Logic in the Programatica Project to provide a verification logic for Haskell

--------------------Reason (3)------------------

There is no formal specification for the meaning of a Haskell program (i.e. its meaning is not defined in a logic). At the level of precise logical specification and logical interoperability this could be a problem (e.g. semantic web likes logic). This should not be a problem for programming tasks, after all most languages like Java do not have a formal semantic definition in logic (like Maude or CafeOBJ ).

In this paper, Yaroslav D. Sergeyev describes a "new computational methodology for executing calculations with infinite and infinitesimal quantities". In his computational model, he introduces infinite types ("units of measure"). Not only does he claim the originality of this approach, he also claims to have patented the "infinity computer" in the European Union. While his approach seems an interesting contribution in general, the calculation with unknowns seems not exactly without predecessor. Besides, I wonder how is this tenable, as algorithms and computer programs are excluded from patent in European law, even more so if they are related to abstract entities. While I could not find any reference to any programming paradigms in the papers available, it may be worth a discussion here.

I embedded jones forth in C programs on windows using masm and/or visual studio.

I am interested to make evolve this forth.
I want to use it as dynamic interpreter to modify C program dynamically. This interpreter has a very small footprint suitable to join it to html files.

is anyone interested to make evolutions to this forth?

I just realized that I first posted about my programming language Heron here on Lambda-the-Ultimate.org over five years ago. Kind of funny to think that at the time then I didn't even know where the name "Lambda the Ultimate" came from. I have learned a lot since, and in no small part thanks to the insights of the brilliant and helpful people at this site!

I have spent the last year, completely redesigning Heron and I have come up with a language which is inspired by a slew of other languages. It is still a curly brace language, with a run-of-the-mill Java style object-oriented approach (minus virtual functions) plus some functional features. In fact it looks a lot like JavaScript 4.0 without prototypes. However, I think that the potentially most interesting feature is the new meta-programming system. Or is it a macro system? I don't actually know, which is why I am writing here.

The idea behind the Heron metaprogramming system is quite simple: a Heron program has two entry points. One for run-time execution, and another for compile-time execution. The only difference between the two entry points, is that the compile-time execution is passed a reference to the abstract syntax tree. At run-time, the modified version of the abstract syntax tree is what gets executed.

You can see this article for a more detailed description if you want, or just look at this Quine demo which prints its own source code out at compile-time.

So I have a couple of questions for the members here:

1. Is it more accurate to call this a metaprogramming system, a macro system, or a compile-time reflection system?
2. What other programming language metaprogramming facilities most resemble the one I describe here?
3. Am I confused or being unintentionally confusing or misleading in some ways on this topic? I find this whole subject area a bit murky with regards to correct usage of the terminology.

Discussion

The use of continuations in a program generally goes together with the use of multiple stacks. That is because several function stack frames can be active at the same time.

This results in obvious memory management issues, such as deciding the location and the size of these stacks. This document explores the idea of a constant size function stack frame, and the conditions in which it allows for a single stack.

I was not sure how to present my ideas in the forum, so I put them in a PDF document.

Does it make sense to think in terms of constant size function stack frame? Is it useful to have a single stack instead of multiple stacks?

I've been reading through "Extensible records with scoped labels", and I'll soon be rereading Cardelli's "Operations on Records." (should be on Citeseer)

My question is simple: are there language implementations, papers, web pages, lore, (anything?) on analyzing, optimizing and thus efficiently implementing the underlying machine data structures and record operator implementations that implement these elegant record systems?

And while I'm asking, any other LTU'ers interested in these record systems and have any insight to share?

Mucho thanks.

Scott