halt
Henry Baker remarked that "it is impossible to create infinite trees -- i.e., directed cycles -- without side-effects." This article shows limitations of that statement. One can construct cyclic lists and other self-referential values in a pure functional style, without resorting to mutations. Lazy evaluation -- either supported by a language, or emulated -- makes this possible. Lazy evaluation even allows an invocation of a function with an argument that refers to the function's result.
An interesting follow-up article showed various ways to simulate self-referential values and lazy computation in ML (Caml).
Furthermore, we can create DAGs and general cyclic data structures even in a strict pure functional language. The following article "On parent pointers in SXML trees" demonstrates different ways of constructing tree-like data structures with forward and backward pointers. Some of the data structures are general graphs with directed cycles, some of them are DAGs. And yet some of them are genuine trees. How can a recursive data structure have forward and backward pointers and yet only a single path between any two nodes? How can we do that in a strict pure language? The article and the accompanying source code explain. The paradoxical tree is built by a procedure add-thunk-parent-pt, which is defined in section 'Solution 3' of the source code. The procedure is deceptively simple. It took 21 lines of Scheme code to implement the algorithm and 26 (full-length) lines of comments to explain it.
A USENET article Self-referential values and
expressiveness of strict vs. non-strict languages [plain text file]
The article was posted on newsgroups comp.lang.scheme,
comp.lang.functional on Mon Feb 14 20:14:49 2000 GMT
Unitary type as a self-referential set
Pure-functional transformations of cyclic graphs and the Credit Card Transform
Henry G. Baker: Equal Rights for Functional Objects or, The More Things Change, The More They Are the Same
On parent pointers in SXML trees
The article and the accompanying Scheme source code. The
article also explains practical benefits of creating and
manipulating cyclical structures in a side-effect-free manner.
The following article describes a real practical application:
avoiding the explosion of makefile rules in a project that executes
many test cases on many platforms. Each test target is built from its
own set of source code files. Each (Scheme) platform has its own
particular way of assembling source code files into a project; some
source code files might need be omitted from the build for a
particular platform. Because GNU make turns out to be a
functional programming system, we can reduce the number of rules from
<number-of-targets> * <number-of-platforms> to just
<number-of-targets>+ <number-of-platforms>.
The language of GNU make is indeed functional, complete with combinators (map and filter), applications and anonymous abstractions. GNU make does support lambda-abstractions. The following is one example from the Makefile in question: it is a rule to build a test target for the SCM Scheme system. The list of source code files and the name of the target/root-test-file are passed as two arguments of the rule:
make-scmi= scm -b -l $(LIBDIR)/myenv-scm.scm \
$(foreach file,$(1),-l $(LIBDIR)/$(file)) \
-l $(2).scm
The rule returns an OS command to interpret or compile the target.
The rule can be invoked as
$(call make-scmi,util.scm catch-error.scm,vmyenv). As in TeX, the arguments of a function are numbered (it is
possible to assign them meaningful symbolic names, too). Makefile's foreach corresponds to Scheme's map. The comparison
with the corresponding Scheme code is striking: (define make-scmi
(lambda (arg1 arg2)
`(scm -b -l ,(mks LIBDIR '/ 'myenv-scm.scm)
,@(map (lambda (file) `(-l ,(mks LIBDIR '/ file))) arg1)
-l ,(mks arg2 '.scm))))
SSAX updates; Makefile as a functional program [plain text file]
A message describing the motivation for the functional Makefile to
automate regression testing, and a few examples. The message was
posted on the SSAX-SXML mailing list on Mon, 18 Nov 2002 12:48:41
-0800
Makefile [7K]
The Makefile in question
Chapter 'Functions' from make info pages.
Konrad Zuse's Z3 was far ahead of its time. Unlike ENIAC, it was controlled by a software program. In Z3, the numbers were represented in a floating point format greatly resembling the one in the IEEE Floating-Point standard. Z3 had two ALUs so it operated on the exponent and the mantissa of a number in parallel.
It appears Z3 was farther ahead than we might have realized. Z3 had no branch instruction and instead relied on predicated execution. The latter technique -- implemented in the most recent upscale CPUs -- is considered to be ``one of the most significant [recent] advances in the history of computer architecture and compiler design.'' It seems that advance is not recent at all: it was invented by Konrad Zuse back in 1938. The letter to Dr.Dobbs J. Editors gives more details.
Simulating Konrad Zuse's Computers
Raul Rojas
Dr. Dobbs J., September 2000, pp. 64-69.
Zuse Accolades [plain text file]
The letter to the editor regarding the above article. It was published in Dr. Dobbs J., December 2000, p. 10.
Zuse and Intel
A letter from reader Ben Laurie
Dr. Dobbs J., August 2001, p. 12.
Ben Lauri points out that Acorn's ARM chip has had the predicated
execution feature more than a decade ago.
Konrad Zuse Internet Archive
<http://www.zib.de/zuse/English_Version/index.html>
A logic programming system with first-class relations and the complete decision procedure (e.g., Kanren) can define the pure Hindley-Milner typechecking relation for a language with polymorphic let, sums and products. The typechecking relation relates a term and its type: given a term we obtain its type. It can also work in reverse: given a type, we can obtain terms that have this type. Or, we can give a term with blanks and a type with blanks, and ask the relation to fill in the blanks.
The code below implements this approach. We use Scheme
notation for the source language (we could just as well supported ML
or Haskell-like notations). The notation for type terms is infix, with
the right-associative arrow. As an example, the end of the file
type-inference.scm shows the derivation for call/cc,
shift and reset from their types in the
continuation monad. Given the type:
(define (cont a r) `((,a -> . ,r) -> . ,r))
(((a -> . ,(cont 'b 'r)) -> . ,(cont 'b 'b)) -> . ,(cont 'a 'b))
within 2 milli-seconds, we obtain the term for shift: (lambda (_.0) (lambda (_.1)
((_.0 (lambda (_.2) (lambda (_.3) (_.3 (_.1 _.2)))))
(lambda (_.4) _.4))))
From Curry-Howard correspondence, determining a term for a type is tantamount to proving a theorem -- in intuitionistic logic as far as our language is concerned. We formulate the proposition in types, for example:
(define (neg x) `(,x -> . F))
(,(neg '(a * b)) -> . ,(neg (neg `(,(neg 'a) + ,(neg 'b)))))
This is one direction of the deMorgan law. In intuitionistic logic,
deMorgan law is more involved:NOT (A & B) == NOTNOT (NOT A | NOT B)The system gives us the corresponding term, the proof:
(lambda (_.0)
(lambda (_.1)
(_.1 (inl (lambda (_.2)
(_.1 (inr (lambda (_.3) (_.0 (cons _.2 _.3))))))))))
The de-typechecker can also prove theorems in classical logic, via the double-negation (aka CPS) translation. We formulate a proposition:
(neg (neg `(,(neg 'a) + ,(neg (neg 'a)))))and, within 403 ms, obtain its proof:
(lambda (_.0) (_.0 (inr (lambda (_.1) (_.0 (inl _.1))))))The proposition is the statement of the Law of Excluded Middle, in the double-negation translation.
Programming languages can help in the study of logic.
type-inference.scm [19K]
Kanren code for the pure Hindley-Milner type inference relation which relates a term in lambda-calculus with
fixpoint, polymorphic let, sums and products -- and its
type. The code contains many comments that explain the notation, the
incremental composition of the typechecking relation and taking the
advantage of the first-class status of Kanren relations for
typechecking of polymorphic let.
logic.scm [9K]
Kanren code that illustrates the application of the inverse
typechecker to proving theorems in intuitionistic and classical
logics.
The Kanren project
<http://kanren.sourceforge.net>
We expound a view of type checking as evaluation with `abstract
values'. Whereas dynamic semantics, evaluation, deals with (dynamic)
values like 0, 1, etc., static semantics, type-checking, deals with
approximations like int. A type system is sound if it
correctly approximates the dynamic behavior and predicts its outcome:
if the static semantics predicts that a term has the type int, the dynamic evaluation of the term, if it terminates, will
yield an integer.
Conventional type-checking is big-step evaluation in the
abstract: to find a type of an expression, we fully `evaluate' its
immediate subterms to their types. We propose a different kind of type
checking that is small-step evaluation in the abstract: it unzips (pun
intended: cf. Huet's zipper) an expression into a context and a
redex. The type-checking algorithms in the paper are implemented in
Twelf; the complete code is available. In particular, the
well-commented file lfix-calc.elf implements, by way of
introduction and comparison, small-step type-checking for simply typed
lambda calculus.
The benefit of small-step typechecking is that, by `following' the control flow, it is more suitable for effectful computations. A more interesting result comes from the fact that static evaluation, unlike the dynamic one, goes `under lambda'. Thus the small-step static evaluation context is a binding context.
Colon becomes the new turnstile! Since the evaluation context is neither commutative or associative but is subject to focusing rules, we obtain the framework for expressing various substructural and modal logics.
Joint work with Chung-chieh Shan.
A Substructural Type System for Delimited Continuations
This paper introduced small-step typechecking when
designing the first sound type system for dynamic delimited
continuations.
small-step-typechecking.tar.gz [10K]
Commented Twelf code with small small-step typechecking
algorithms and many sample derivations.
Abstract interpretation in the denotational context:
Patrick Cousot, Types as abstract interpretations. POPL 1997, 316-331.
Abstract interpretation as an aid during program development
of logical programs:
Manuel Hermenegildo, Germa'n Puebla, and Francisco Bueno:
Using global analysis, partial specifications, and an extensible
assertion language for program validation and debugging.
In The logic
programming paradigm: A 25-year perspective, ed. Krzysztof R. Apt,
Victor W. Marek, Mirek Truszczynski, and David S. Warren, 161-192,
1999. Berlin: Springer-Verlag.
The following short essay argues that the Axiom of Choice can be regarded as a deconstructor (i.e., cursor-like) API for a set. In contrast, axioms of (restricted) comprehension and of replacement are more like the enumerator API for a set. The Axiom of Choice does not reveal how the set in question has been constructed. The Axiom of Choice may also be viewed as an assertion that set's membership predicate is safe, in Dalatog sense.
In a more recent discussion, Neelakantan Krishnaswami
introduced a choose function as an indispensable part of
an API for a Set, enabling us to reason about sets
algebraically and equationally.
The essay [plain text file]
Neelakantan Krishnaswami. Re: FP-style map over set
<http://groups.google.com/group/comp.lang.functional/msg/9066226001187a0a>
A message posted on a newsgroup comp.lang.functional
on Mon, 28 Nov 2005 23:45:27 +0000 (UTC)
This article proves by construction that sendmail rewriting rules are Turing-complete. They are expressive enough to implement a Turing machine. The article first gives an introduction to the rewriting rules, for easy reference. We then explain how to map Turing machine configuration (the content of the tape and the current position) to a character string, and machine's finite control to rewriting rules. As an example, we demonstrate two Turing machines: an adder of two natural numbers, and an even/odd decision function. We explain how to run these examples and see the result.
The USENET article itself [plain text file]
This article, Sendmail as a Turing machine, was posted on
newsgroups comp.lang.functional and comp.mail.sendmail on Sun, 10 Sep 2000 22:26:33 GMT
sendmail.cf [37K]
A sendmail configuration file (sendmail.cf) augmented with rules to
implement the Turing machine. This file also defines two sample Turing
machines.
The following archive contains a simple implementation of Turing machine in Standard ML (SML/NJ). For illustration, the code includes three sample Turing programs: the successor function, a character substitution function, and a decision function. For example,
- turing_machine((0,["#","a","a","a","a","a","a"],"#",[]),prog_decision);
val it = (~1,["#","Yes"],"#",["#","#","#","#","#"])
: int * string list * string * string list
shows that starting the decision program (which decides if a string
contains an even number of characters) with the tape
#aaaaaa###.... and the head positioned at the beginning
of the tape, leaves # "YES" ####... on the tape after
the machine halts (by reaching the state -1). Thus, the machine has
decided the input string contained an even number of characters.This site's top page is http://pobox.com/~oleg/ftp/
Converted from SXML by SXML->HTML