Home

PCF and LCF

The theory LCF, for Logic of Computable Functions, was proposed by Dana Scott as a theory in the spirit of Church's simple theory of types which allows the computable functions to be characterised, and which comes with a rich enough logical theory to be analytically useful.

PCF, the Programming with Computable Functions toy language, was proposed by Robin Milner in an exposition of Scott's work on LCF.

The two formalisms have been enormously fruitful in theoretical computer science, and I've noticed that two of the early seminal papers are available as scanned PDFs:

Dana Scott's original 1969 manuscript, A theory of computable functions of higher type was, I believe, only ever circulated informally, and I've never got hold of the manuscript in any form.

By Charles Stewart at 2007-04-14 07:29 | Type Theory | other blogs | 19778 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

It occurs to me that we

It occurs to me that we never really discussed LCF on LtU. Among the various technical concepts often found in PLT papers, LCF is one of the few that were never explained and discussed here on an introductory level. Thanks for fixing that!

By Ehud Lamm at Sat, 2007-04-14 11:46 | login or register to post comments

I'm already stuck on page 2 of Models of LCF

f is continuous if it preserves the union of chains. (I'm using 'union' to mean the thing represented by a square union symbol.) But implicit in that definition is that the image of a chain is a chain. Milner anticipates my objection by pointing out that the image of a chain is in fact a chain. But to do that he uses the union of { f(x), f(y) }. But this isn't a chain (after all we're trying to prove this), so how can I form its union? The definition of a cpo assumes only that chains have an l.u.b. The only conclusion I can come to is that implicit in the definition of a continuous function f is the additional assumption that for all x and y in the domain of f, f(x) and f(y) always have a l.u.b.

What did I miss in pages 1 and 2?

By sigfpe at Sun, 2007-04-15 00:28 | login or register to post comments

Isn't this right there on the definition?

I may be missing something, but isn't this right there on the definition of a continuous function? It says that if X is a chain then U{f(x): x in X} = f(UX). So the definition states that if X is a chain, its image has a lub. It uses this fact in the proof that U{f(x) : x in X} is a chain, because if Y = {x, y} is a chain then UY = y; so, by the definition of a continuous function, U{f(x), f(y)} = f(UY) = f(y), and by the properties of partial order and a lub, f(x) <= U{f(x), f(y)}, so f(x) <= f(y), so a continuous function is monotonic and thus U{f(x), f(y)} is a chain.

Is this right? What am I missing?

By Andrei Formiga at Sun, 2007-04-15 01:24 | login or register to post comments

I think that clarifies things

So I should read definition 2.4 with this in mind:


  1. it's implicitly stating that a condition for f to be a continuous functions is that its image has a l.u.b. and
  2. U is used to mean the l.u.b. of a set despite being explicitly defined as a function on chains

OK, that makes sense.

By sigfpe at Sun, 2007-04-15 01:40 | login or register to post comments

Oddly circular

In the end, the set ends up being a chain, by force of the definition. I had noticed this odd circularity in this definition, but I don't know what to make of it.

By Andrei Formiga at Sun, 2007-04-15 02:52 | login or register to post comments

A bit sloppy

I find it a sloppy writing style. Just about every mathematics text I know that does something like this has a phrase like "...the l.u.b. exists and..." inserted in there. Similarly, over the page he says "Define UZ = ...". UZ is already defined. What he really means is that the rhs exists and is the l.u.b. But it's certainly not a definition. Normally I'm not so picky but this is foundational stuff so details matter. I guess that by time I reach the end everything will make perfect sense in hindsight.

By sigfpe at Mon, 2007-04-16 18:49 | login or register to post comments

Stanford LCF

Ah, another scan:

This paper is more expository in tone than Milner's other TR, so it might be easier going for those engaging in close reading, plus this scan is maybe a little easier to read.

If anyone knows of an online version of the original Edinburgh LCF paper, that would certainly be worth posting!

By Charles Stewart at Tue, 2007-04-17 21:29 | login or register to post comments

LCF ur-manuscript...

A theory of computable functions of higher type was published with annotations as Scott, 1993, A Type-Theoretical Alternative to ISWIM, CUCH, OWHY (scan). See my request on cstheory, which Scott answered.

By Charles Stewart at Thu, 2011-06-09 21:20 | login or register to post comments