Programming Computable Functions (PCF)

PCF is a call-by-name simply-typed \lambda-calculus equipped with

one or two base types (usually flat natural numbers and Booleans)
a fixed point combinator at all types

In essence, PCF is the simplest lazy, purely functional programming language. This allows it to serve as a basis for programming language research.

Type system

At a bare minimum, the types of PCF consist of the natural numbers, and function types:

\sigma, \tau\ ::=\ \mathbb{N} \mid \sigma \to \tau

There are of course variations. Most commonly, these include a type \mathbb{B} of Booleans, products, (weak) sums, and so on.

The natural numbers are introduced by constants, one for each natural:

\frac{
n \geq 0
}{
\Gamma \vdash \underline{n} : \mathbb{N}
}

This presentation is called flat. It is necessary to avoid non-standard, lazy numbers, e.g. \textsf{succ}(\bot) where \bot is a non-terminating progrram.

Natural numbers are manipulated by some basic functions: the successor, the predecessor, and a test-if-zero:

\frac{
}{
  \Gamma \vdash \textsf{succ} : \mathbb{N} \to \mathbb{N}
}
  \quad
\frac{
}{
  \Gamma \vdash \textsf{pred} : \mathbb{N} \to \mathbb{N}
}

\frac{
  \Gamma \vdash M : \mathbb{N}
  \quad
  \Gamma \vdash P : A
  \quad
  \Gamma \vdash Q : A
}{
 \Gamma \vdash \textsf{ifz}\ M\ \textsf{then}\ P\ \textsf{else}\ Q\ : A
}

As usual, function types are introduced and eliminated by \lambda-abstraction and application:

\frac{
  \Gamma, x : A \vdash M : B
}{
  \Gamma \vdash \lambda x : A.\, M : A \to B
}
  \quad
\frac{
  \Gamma \vdash M : A \to B
  \quad
  \Gamma \vdash N : A
}{
  \Gamma \vdash M(N) : B
}

Finally, PCF postulates the existence of a fixed-point combinator at all types. This is sometimes presented as a constant \mathbb{Y} : (A \to A) \to A. Here we present it equivalently as a binding construct:

\frac{
  \Gamma, x : A \vdash M : A
}{
  \Gamma \vdash \textsf{fix}\ x.\ M : A
}

Operational semantics

Please expand.

Models

There are many (denotational) models of PCF: see the main article.

The correspondence between the operational behaviour of PCF and its denotational models leads to infamous full abstraction problem.

Call-by-value variant

Please expand.

References

The first explicit formulation of PCF originated in a famous unpublished 1969 manuscript of Dana Scott, which was eventually published in 1993. In its original form it was not a \lambda-calculus, but a system of combinatory logic. The impetus was Scott's frustration at the lack of a good semantics for the untyped \lambda-calculus. The system itself is strongly inspired by Richard Platek's 1966 PhD thesis.

Scott, Dana S. 1993. ‘A Type-Theoretical Alternative to ISWIM, CUCH, OWHY’. Theoretical Computer Science 121 (1–2): 411–440. https://doi.org/10.1016/0304-3975(93)90095-B.

@article{scott_type-theoretical_1993,
	title = {A type-theoretical alternative to {ISWIM}, {CUCH}, {OWHY}},
	volume = {121},
	issn = {03043975},
	doi = {10.1016/0304-3975(93)90095-B},
	number = {1-2},
	journal = {Theoretical Computer Science},
	author = {Scott, Dana S.},
	year = {1993},
	pages = {411--440}
}

Scott's combinator system was later presented as a typed \lambda-calculus by Gordon Plotkin. It was then equipped with both an operational semantics and a denotational semantics. The operational semantics is shown to be sound with respect to the denotational semantics, and also adequate, which is a form of weak completeness. There are many further results relating to the expressivity of the language: see universality.

Plotkin, Gordon D. 1977. ‘LCF Considered as a Programming Language’. Theoretical Computer Science 5 (3): 223–255. https://doi.org/10.1016/0304-3975(77)90044-5.

@article{plotkin_lcf_1977,
	title = {{LCF} considered as a programming language},
	volume = {5},
	doi = {10.1016/0304-3975(77)90044-5},
	number = {3},
	journal = {Theoretical Computer Science},
	author = {Plotkin, Gordon D.},
	year = {1977},
	pages = {223--255}
}

The first full abstraction result for PCF was given by Milner. Unfortunately, the model was syntactic, so no additional insight was offered by this result - except a curious result: the syntactic model is the unique order-extensional fully abstract model.

Milner, Robin. 1977. ‘Fully Abstract Models of Typed λ-Calculi’. Theoretical Computer Science 4 (1): 1–22. https://doi.org/10.1016/0304-3975(77)90053-6.

@article{milner_fully_1977,
	title = {Fully abstract models of typed λ-calculi},
	volume = {4},
	issn = {03043975},
	doi = {10.1016/0304-3975(77)90053-6},
	number = {1},
	journal = {Theoretical Computer Science},
	author = {Milner, Robin},
	year = {1977},
	pages = {1--22}
}

Textbook presentations of PCF include

Harper, Robert. Practical Foundations for Programming Languages. 2nd ed. Cambridge: Cambridge University Press, 2016. doi:10.1017/CBO9781316576892.

@book{harper_practical_2016,
  title     = {Practical {Foundations} for {Programming} {Languages}},
  publisher = {Cambridge University Press},
  year      = {2016},
  author    = {Harper, Robert},
  address   = {New York, NY, USA},
  edition   = {Second},
  isbn      = {978-1-107-15030-0},
  doi       = {10.1017/CBO9781316576892}
}

Streicher, Thomas. 2006. Domain-Theoretic Foundations of Functional Programming. World Scientific.

@book{streicher_domain-theoretic_2006,
	title = {Domain-theoretic {Foundations} of {Functional} {Programming}},
	publisher = {World Scientific},
	author = {Streicher, Thomas},
	year = {2006}
}

Mitchell, John C. 1996. Foundations for Programming Languages. Foundations of Computing. The MIT Press.

@book{mitchell_foundations_1996,
	series = {Foundations of {Computing}},
	title = {Foundations for programming languages},
	isbn = {978-0-262-13321-0},
	publisher = {The MIT Press},
	author = {Mitchell, John C.},
	year = {1996}
}

Gunter, Carl A. 1992. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing. MIT Press.

@book{gunter_semantics_1992,
	series = {Foundations of {Computing}},
	title = {Semantics of {Programming} {Languages}: {Structures} and {Techniques}},
	isbn = {978-0-262-57095-4},
	publisher = {MIT Press},
	author = {Gunter, Carl A.},
	year = {1992}
}

Fully abstract models of PCF were first described by

Abramsky, Samson, Radha Jagadeesan, and Pasquale Malacaria. 1996. ‘Full Abstraction for PCF’. Information and Computation 163: 409–70. arXiv

@article{abramsky_full_1996,
	title = {Full {Abstraction} for {PCF}},
	volume = {163},
	journal = {Information and Computation},
	author = {Abramsky, Samson and Jagadeesan, Radha and Malacaria, Pasquale},
	year = {1996},
	pages = {409--470}
}

Hyland, J.M.E., and C.-H.L. Ong. 2000. ‘On Full Abstraction for PCF: I, II, and III’. Information and Computation 163 (2): 285–408. https://doi.org/10.1006/inco.2000.2917. pdf

@article{hyland_ong_2000,
	title = {On {Full} {Abstraction} for {PCF}: {I}, {II}, and {III}},
	volume = {163},
	url = {http://linkinghub.elsevier.com/retrieve/pii/S0890540100929171},
	doi = {10.1006/inco.2000.2917},
	number = {2},
	journal = {Information and Computation},
	author = {Hyland, J.M.E. and Ong, C.-H.L.},
	year = {2000},
	pages = {285--408}
}

Nickau, Hanno. 1994. ‘Hereditarily Sequential Functionals’. In Logical Foundations of Computer Science, edited by Anil Nerode and Yu. V. Matiyasevich, 813:253–64. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-58140-5_25.

@inproceedings{nickau_1994,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Hereditarily sequential functionals},
	volume = {813},
	doi = {10.1007/3-540-58140-5_25},
	booktitle = {Logical {Foundations} of {Computer} {Science}},
	publisher = {Springer Berlin Heidelberg},
	author = {Nickau, Hanno},
	editor = {Nerode, Anil and Matiyasevich, Yu. V.},
	year = {1994},
	pages = {253--264}
}