Lambda the Ultimate

This week there were two item in the tech blogs that were both programming language and both related; the 'Radiation resistant Quine' and the Apple SSL error caused. Both deal with a small number of characters and the resilience of the program and language to errors.

It raises a question - can we build resilience into our programming languages?

I think we can build more resilient programs, the ruby example was designed to be resilient, but as far as I know resilience is not a feature of Ruby, any more than it is C.

Any thoughts?

I have devoted a lot of time trying to understand why a book like "Algebraic Structure Theory of Sequential Machines" is nearly unknown. The book is written by two great Computer Scientists, Hartmanis and Stearns; one of whom, Hartmanis, started the first Computer Science program at an American university. Surely there is a story here.

The situation seems to develop out of the cultural chaos of the 1960's. The HandS book seems to be collateral damage. In 1965 students are rioting on campuses all across America. Professors are being fired if they show any sympathy for this behavior at all. Loosely allied with all this is the academic theory of information and Cybernetics. Now it just so happens that the HandS book is probably one of the best books on information or cybernetics ever written. It could be that the politically astute students and professors know enough to stay away from anything that smells like Cybernetics. It is just a theory mind you. It has been nearly 50 yerrs how. My how time flies. I think it is time to take a fresh look at this book.

Inconsistency Robustness requires repairing mathematical foundations in the face of contradictions that have arisen over and over again. In the Inconsistency Robustness paradigm, deriving contradictions are a progressive development and not “game stoppers.” Contradictions can be helpful instead of being something to be “swept under the rug” by denying their existence, which has been repeatedly attempted by the Establishment (beginning with some Pythagoreans). Such denial has delayed mathematical development. This article reports how Inconsistency Robustness has recently influenced the foundations of mathematics for Computer Science since the first International Symposium in 2011 continuing a tradition developing the sociological basis for foundations.

That mathematics is thought to be consistent by an overwhelming consensus of working professional mathematicians justifies the use of Proof by Contradiction. In addition, Proof by Contradiction can be used to infer the consistency of mathematics by the following simple proof:

The self-proof is a proof by contradiction.
In order to obtain a contradiction,
assume that mathematics is inconsistent.
Then there is some proposition Φ such that ⊢Φ and ⊢¬Φ.
Consequently, both Φ and ¬Φ are theorems that
can be used in the proof to produce an immediate contradiction.
Therefore mathematics is consistent.

Please note the following points: The above argument mathematically proves the theorem that mathematics is consistent and that it is not a premise of the theorem that mathematics is consistent. However, the proof does not intuitively increase our confidence in the consistency of mathematics because it does not rule out that there might be other proofs in mathematics that result in contradictions.

The above theorem means that the assumption of consistency is deeply embedded in the architecture of classical mathematics. The above proof of consistency can be formalized in Direct Logic [Hewitt 2010] (a powerful inference system in which computer systems can reason about their own inferences). Having a powerful system like Direct Logic is important in computer science because computers must be able to carry out all inferences (including inferences about their own inference processes) without requiring recourse to human intervention.

Self-proving consistency raises that possibility that mathematics could be inconsistent because of contradiction with the result of Gödel et. al. that if mathematics is consistent, then it cannot infer its own consistency. The resolution is to provide a proper grammar of mathematical sentences so that a fixed-point operator cannot be used to construct the kind of “self-referential” proposition used by Gödel in his results by exploiting an untyped grammar of sentences. Self-referential propositions of the kind used by Gödel do not seem to have any important practical applications. (There is a very weak theory called Provability Logic that has been used for self-referential propositions coded as integers, but it is not strong enough for the purposes of computer science.) Direct Logic makes use of a typed grammar that prevents the construction of self-referential sentences using unwanted fixed points. The bottom line is that self-referential propositions are “monsters” (in the sense of Lakatos) that are ruled about by a proper grammar of sentences for the mathematical foundations of computer science. It is important to note that not having self-referential propositions does not place restrictions on recursion in computation, e.g., the Actor Model, untyped lambda calculus, etc.

A mathematical theory is an extension of mathematics whose proofs are computationally enumerable. For example, group theory is obtained by adding the axioms of groups to Direct Logic along with the requirement that proofs are computational enumerable. If a mathematical theory T is consistent, then it is inferentially undecidable (i.e. there is a proposition Ψ such that ⊬_TΨ and ⊬_T¬Ψ (which is sometimes called “incompleteness” in classical terminology) because provability in T is computationally undecidable [Church 1936, Turing 1936].

Information Invariance is a fundamental technical goal of logic consisting of the following:
1. Soundness of inference: information is not increased by inference
2. Completeness of inference: all information that necessarily holds can be inferred
Direct Logic aims to achieve information invariance for the mathematical foundations of Computer Science. But that a mathematical theory is inferentially undecidable (“incomplete” in classical terminology) with respect to Ψ (above) does not mean incompleteness with respect to the information that can be inferred because (by construction) it is provable in mathematics that ⊬_TΨ and ⊬_T¬Ψ.

This article has become highly controversial and the Establishment has censored (without substantive justification) its publication in electronic archives that are intended to record priority dates for scientific results. Consequently, this article is itself another episode in the ongoing saga of inconsistency robustness in foundations.

The article for the above abstract can be found here: Inconsistency Robustness in Foundations

"Algebraic Structure Theory of Sequential Machines" will seem hopelessly out of date to some people, but the contemporary interest in concurrency gives the book a new found importance. I have a complete searchable scan of the book that I would post online if I knew how to get permission from Prentice-Hall. Does anyone have any ideas?

Here is the very interesting preface of the book.

The explosive development of information-processing technology during
the last two decades has stimulated the vigorous growth of an Information
Science. This new science is primarily concerned with the study of information
and the laws which govern its processing and transmission. A very
active part of this science is the study of sequential machines or finite automata
which are abstract models of digital computers. The aim of this research
is to provide a basic theoretical background for the study of digital computers
and to contribute to a deeper understanding of discrete or finite
information-processing devices. This area of research was started around
1954 by D. A. Huffman and E. F. Moore and has since undergone a considerable
growth in several diverse directions. In the period from 1960 to
1965, a body of results we call "structure theory" was created and developed
to a considerable degree of completeness and unity. This book is an exposition
on the foundations, techniques, and applications of this theory.

By a structure theory for sequential machines, we mean an organized
body of techniques and results which deal with the problems of how sequential
machines can be realized from sets of smaller component machines, how
these component machines have to be interconnected, and how "information"
flows in and between these machines when they operate. The importance of
machine structure theory lies in the fact that it provides a direct link between
algebraic relationships and physical realizations of machines. Many structure
results describe the organization of physical devices (or component machines)
from which a given machine can be synthesized. Stated differently, the
structure theory describes the patterns of possible realizations of a machine
from smaller units. It should be stressed, however, that although many
structure theory results describe possible physical realizations of machines,
the theory itself is independent of the particular physical components or
technology used in the realization. More specifically, this theory is concerned
with logical or functional dependence in machines and studies the information
flow of the machine independently of how the information is represented
and how the logical functions are to be implemented.

The mathematical foundations of this structure theory rest on an algebraization
of the concept of "information" in a machine and supply the algebraic
formalism necessary to study problems about the flow of this information
in machines as they operate. The formal techniques and results are
very closely related to modern algebra. Many of its results show considerable
similarity with results in universal algebra, and some can be directly derived
from such considerations. Nevertheless, the engineering motivation demands
that this theory go its own way and raises many problems which require
new mathematical techniques to be invented that have no counterpart in
the development of algebra. Thus, this theory has a characteristic flavor and
mathematical identity of its own. It has, we believe, an abstract beauty
combined with the challenge and excitement of physical interpretation and
application. It falls squarely in the interdisciplinary area of applied algebra
which is becoming a part of engineering mathematics.

This book is intended for people interested in information science
who have either an engineering or mathematical background. It can be read
by anyone who has either some mathematical maturity, achieved through
formal study, or engineering intuition developed through work in switching
theory or experience in practical computer design.

Enough concepts of machine theory and machine design are introduced
in the first chapter so that a mathematician may read the book without any
experience with computers or switching theory. A preliminary chapter on
basic algebraic concepts supplies enough mathematics to make the book
self-contained for a non-mathematician. A good number of examples are
given to supply the engineer with an interpretation or application of the
mathematics.
J. HARTMANIS
R. E. STEARNS

Anyone tried hopscotch?

Only recently when I started posting things here I realized that I have to use HTML for any formatting, which is too verbose. How about switching to Markdown? This requires a Markdown-to-HTML converter (Pandoc is the best) running on the server side. The cost can be shared.

I came across an early post on the topic of disallowing shadowing (message quoted below):

In lambda calculus you can always rebind an already-bound name, but in
practice, there are lots of limitations imposed on rebinding in real
languages: top-level module bindings can't be redefined in mzscheme,
operations of type classes can't be redefined at the top level in
Haskell, etc. What happens if you take this to the extreme and disallow
shadowing entirely in a lexically scoped language? [1]

At first I thought this would cause problems for macros, but in a
hygienic system that renames everything to something fresh anyway, it
probably wouldn't matter.

Other than being an annoyance when you want to reuse a name for some
other purpose (which is arguably bad style anyway), what problems would
disallowing local rebinding cause?

Dave

[1] http://www.mail-archive.com/haskell@haskell.org/msg01268.html

There were a few follow-up discussions but did not expand further. Essentially I have the same question as Dave and I hope to hear more comments on it.
What is theoretical and practical consequence, say if we forbid shadowing in the lambda caluclus?

I noticed that CoffeeScript has gone toward the direction of forbid shadowing. Although raised a lot of opposition, the designer insisted on it. Is his point solid?

The Actor model is a mathematical theory that treats “Actors” as the universal primitives of concurrent digital computation. The model has been used both as a framework for a theoretical understanding of concurrency, and as the theoretical basis for several practical implementations of concurrent systems. Unlike previous models of computation, the Actor model was inspired by physical laws. It was also influenced by the programming languages Lisp, Simula 67 and Smalltalk-72, as well as ideas for Petri Nets, capability-based systems and packet switching. The advent of massive concurrency through client-cloud computing and many-core computer architectures has galvanized interest in the Actor model.

An Actor is a computational entity that, in response to a message it receives, can concurrently:
• send messages to addresses of Actors that it has;
• create new Actors;
• designate how to handle the next message it receives.

There is no assumed order to the above actions and they could be carried out concurrently. In addition two messages sent concurrently can be received in either order. Decoupling the sender from communication it sends was a fundamental advance of the Actor model enabling asynchronous communication and control structures as patterns of passing messages.

The Actor model can be used as a framework for modeling, understanding, and reasoning about, a wide range of concurrent systems. For example:
• Electronic mail (e-mail) can be modeled as an Actor system. Mail accounts are modeled as Actors and email addresses as Actor addresses.
• Web Services can be modeled with endpoints modeled as Actor addresses.
• Objects with locks (e.g. as in Java and C#) can be modeled as Actors.
• Functional and Logic programming implemented using Actors.

Actor technology will see significant application for integrating all kinds of digital information for individuals, groups, and organizations so their information usefully links together. Information integration needs to make use of the following information system principles:
• Persistence. Information is collected and indexed.
• Concurrency: Work proceeds interactively and concurrently, overlapping in time.
• Quasi-commutativity: Information can be used regardless of whether it initiates new work or become relevant to ongoing work.
• Sponsorship: Sponsors provide resources for computation, i.e., processing, storage, and communications.
• Pluralism: Information is heterogeneous, overlapping and often inconsistent. There is no central arbiter of truth
• Provenance: The provenance of information is carefully tracked and recorded

The Actor Model is intended to provide a foundation for inconsistency robust information integration.

See article at following location: Parallelism and Concurrency in the Actor Model

Interesting observation that the state comonad (sometimes known as the product comonad) and exception monad are dual:

T A = A × X (state comonad)
T A = A + X (exception monad)

A duality between exceptions and states

The duality between categorical products and sums can be extended as a duality between the semantics of the lookup and update operations for states on one side and the semantics of the constructor [throw] and recovery operations [catch] for exceptions on the other side.

Verification games: Making verification fun

Abstract:
Program verification is the only way to be certain that a given piece of software is free of (certain types of) errors — errors that could otherwise disrupt operations in the field. To date, formal verification has been done by specially-trained engineers. Labor costs have heretofore made formal verification too costly to apply beyond small, critical software components.

Our goal is to make verification more cost-effective by reducing the skill set required for program verification and increasing the pool of people capable of performing program verification. Our approach is to transform the verification task (a program and a goal property) into a visual puzzle task — a game — that gets solved by people. The solution of the puzzle is then translated back into a proof of correctness. The puzzle is engaging and intuitive enough that ordinary people can through game-play become experts.

This paper presents a status report on the Verification Games project and our Pipe Jam prototype game.