Lambda the Ultimate

There's a neat thread about strong normalization happening on The Types Forum.

If you've ever wondered Why is it useful to have {type systems,reductions,operations,...} that always terminate? this may Illuminate you.
Here are some snippets to give you a feel for the discussion:

I think it is clearer to split Gérard's original question in two:

1. Is strong normalization useful for programming languages ?
2. Is the proof of strong normalization via type systems applicable for programming languages?

-- François-Régis Sinot

Termination is good:

If a program is a solution to a problem then knowing that it terminates
for any input is an important aspect of it being a solution. Often the
best way to see that it is terminating is expressing it in a language
where all programs terminate. The programming language Epigram is an
example of an experimental language which is intended to be terminating
(even though not all conditions are enforced in the current version), see
http://www.e-pig.org/ for more information.

-- Thorsten Altenkirch

Termination is good!

I think the moral sense of strong normalization is that a program
in a strictly-typed language can only diverge as a result of some
programming construct, which _explicitly_ permits looping, like
iteration, recursion etc. My favourite example here is that the
"big Omega" can be written in Algol 60, because procedure types
in this language are not fully specified.

-- Pawel Urzyczyn

Termination is good and with fixpoints is turing complete?

Another way to put this is that data structures should be definable in a
strongly-normalising language so that data access, etc. is guaranteed to
terminate. Then add fixpoints or loops to describe arbitrary computations.

-- Barry Jay

Terminating reductions allows exhaustive applications of optimizations:

In a compiler, if a set of reductions is strongly normalizing, then the compiler can apply them exhaustively to an intermediate-language term without fear of looping. (We rely on this in the MLj and SML.NET compilers' "simplify" compilation phases, which apply simple reductions and directed commuting conversions until a normal form is reached. Though it has to be said that it's not the classical SN results that are relevant here, but something more specific to our intermediate language and the simplifying reductions that we employ).

-- Andrew Kenney

Rene Vestergaard also gave a link to a 2004 discussion of strong normalization on the rewriting list.

The problem: Most languages don't have formal specifications.

The solution (maybe): Make specification easier by using mechanized tools (for example, use Twelf).

The presentation: here (Robert Harper, ICFP'05).

The conclusion: You decide.

We present a file server/OS where threading and exceptions are all realized via delimited continuations. We use zipper to navigate within any term. If the term in question is a finite map whose keys are strings and values are either strings or other finite maps, the zipper-based file system looks almost the same as the Unix file system. Unlike the latter, however, we offer: transactional semantics; undo of any file and directory operation; snapshots; statically guaranteed the strongest, repeatable read, isolation mode for clients; built-in traversal facility; and just the right behavior for cyclic directory references.



We can easily change our file server to support NFS or 9P or other distributed file system protocol. We can traverse richer terms than mere finite maps with string keys. In particular, we can use lambda-terms as our file system: one can cd into a lambda-term in bash.



The implementation of ZFS has no unsafe operations, no GHC let alone Unix threads, and no concurrency problems. Our threads cannot even do IO and cannot mutate any global state --- and the type system sees to it. We thus demonstrate how delimited continuations let us statically isolate effects even if the whole program eventually runs in an IO monad.

zfs-talk: Expanded talk with the demo. It was originally presented as an extra demo at the Haskell Workshop 2005

ZFS.tar.gz: The complete source code, with comments. It was tested with GHC 6.4 on FreeBSD and Linux


From: Zipper-based file server/OS


Neat, a referentially transparent filesystem with transactional semantics in 540 lines of Haskell. I can think of some interesting uses for this.

The Essence of Dataflow Programming

The abstract:

We propose a novel, comonadic approach to dataflow (streambased) computation. This is based on the observation that both general and causal stream functions can be characterized as coKleisli arrows of comonads and on the intuition that comonads in general must be a good means to structure context-dependent computation. In particular, we develop a generic comonadic interpreter of languages for context-dependent computation and instantiate it for stream-based computation. We also discuss distributive laws of a comonad over a monad as a means to structure combinations of effectful and context-dependent computation. We apply the latter to analyse clocked dataflow (partial streams based) computation.

If you've ever wondered about dataflow or comonads, this paper is a good read. It begins with short reviews of monads, arrows, and comonads and includes an implementation. One feature that stood out is the idea of a higher-order dataflow language.

Unlike the previous approaches, the latest implementation is generic. Shift and control share all the same code, and differ in only one boolean flag. Therefore, it becomes possible to mix different control operators in the same program. Furthermore, the latest implementation is direct rather than emulation (in terms of an object-level shift), therefore, it has the best performance. The code is surprisingly simple, compared with the previous implementation of 'control' by Sitaram and Felleisen, and does not require equality on continuations. All four delimited control operations do indeed reduce to call/cc and one global mutable cell, and hence have a quite simple CPS transform. That has been known since the paper by Chung-chieh Shan (Scheme Workshop, 2004). The current code shows that result more directly.

Oleg's implementation provides all four Friedman-Felleisen delimited control operators: from -F- (similar to cupto) to +F- (aka control) to +F+ (aka shift). The R5RS Scheme code is parameterized by two boolean flags: is-shift and keep-delimiter-upon-effect. All four combinations of the two flags correspond to four delimited control operators.

I found this in my mail.

August 12, 2005

The Publisher and Editorial Board of Information and Computation are pleased to announce that for one year, effective immediately, online access to all journal issues back to 1995 will be available without charge. This includes unrestricted downloading of articles in pdf format. Journal articles may be obtained through the journal's web site http://theory.csail.mit.edu/~iandc or Elsevier's Sciencedirect at http://www.sciencedirect.com/science/journal/08905401

At the end of the year, the retrieval traffic during the open access period will be evaluated as future subscription policies are considered.

Albert R. Meyer, Editor-in-Chief, MIT Computer Science & AI Lab
Chris Leonard, Publishing Editor, Elsevier
Moshe Y. vardi, Associate Editor, Rice University

Those of a more theoretical bent will find lots of interesting articles there.

Trampolining Architectures

A trampolining architecture is a special case and extension of a monad which is useful in implementing multiprogramming. Five trampolining architectures, operating over the range of two trampolining translations, are presented. The effects of the architectures are cumulative. Some increase the breadth of multiprogramming facilities provided. Others demonstrate the potential for more efficient implementation. Finally, we demonstrate the applicability of trampolining to languages without closures.

We discussed more than once Trampolined Style, but never this paper by the same authors (except Wand). Published one year later, it discusses more options, and more importantly, shows relations between trampolines and monads.

If you are interested in design and implementation of PLs, and you never heard about tramplines - you should.

Causal Nets

The network approach to computation is more direct and "physical" than the one based on some specific computing devices (like Turing machines). However, the size of a usual -- e.g., Boolean -- network does not reflect the complexity of computing the corresponding function, since a small network may be very hard to find even if it exists. A history of the work of a particular computing device can be described as a network satisfying some restrictions. The size of this network reflects the complexity of the problem, but the restrictions are usually somewhat arbitrary and even awkward. Causal nets are restricted only by determinism (causality) and locality of interaction. Their geometrical characteristics do reflect computational complexities. And various imaginary computer devices are easy to express in their terms. The elementarity of this concept may help bringing geometrical and algebraic (and maybe even physical) methods into the theory of computations. This hope is supported by the grouptheoretical criterion given in this paper for computability from symmetrical initial configurations.

The nets of this paper are different from belief nets or Bayesian nets, which are also known under name "causal nets".

No doubt, modeling the history of computation rather than the current state is nothing new, but this paper tries to find new applications for that.

Accurate step counting. Catherine Hope and Graham Hutton.

Starting with an evaluator for a language, an abstract machine for the same language can be mechanically derived using successive program transformations. This has relevance to studying both the space and time properties of programs because these can be estimated by counting transitions of the abstract machine and measuring the size of the additional data structures needed, such as environments and stacks. In this article we use this process to derive a function that accurately counts the number of steps required to evaluate expressions in a simple language.

Somewhat related to a recent discussion (in which I mentioned EOPL1's scetion on deriving a compiler and machine from an interpreter).

The paper is, of course, worth checking out regardless.

In 2001, Moshe Vardi organised a workshop devoted to a the topic of The Unusual Effectiveness of Logic in Computer Science with papers presented covering such topics as "Logic as the calculus of computer science" (Vardi) and "Descriptive complexity" (Immerman), and later a gang consisting of Halpern, Harper, Immerman, Kolaitis, Vardi, and Vianu published a likewise named 24 page article in the July 2002 issue of the Bulletin of Symbolic Logic.

The title is derived from Wigner's famous article on The Unreasonable Effectiveness of Mathematics in the Natural Sciences, which was devoted to raising and attempting to answer the important question: why should mathematics have been so useful to natural scientists? With respect to logic, my answer for the effectiveness of LICS is that, while computation is a physical phenomenon, it is a phenomenon that is best understood via powerful abstractions, and the most powerful abstractions we have at the moment are abstractions in mathematical logic, because of the fundamental relationship of Turing completeness to Goedelian incompleteness.

Links derived from Richard Zach's Motivating Intro Logic for Philosophy majors (and others).

More links...