PCF is a call-by-name simply-typed -calculus equipped with
In essence, PCF is the simplest lazy, purely functional programming language. This allows it to serve as a basis for programming language research.
At a bare minimum, the types of PCF consist of the natural numbers, and function types:
There are of course variations. Most commonly, these include a type of Booleans, products, (weak) sums, and so on.
The natural numbers are introduced by constants, one for each natural:
This presentation is called flat. It is necessary to avoid non-standard, lazy numbers, e.g. where is a non-terminating progrram.
Natural numbers are manipulated by some basic functions: the successor, the predecessor, and a test-if-zero:
As usual, function types are introduced and eliminated by -abstraction and application:
Finally, PCF postulates the existence of a fixed-point combinator at all types. This is sometimes presented as a constant . Here we present it equivalently as a binding construct:
Please expand.
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.
Please expand.
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}
}
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}
}
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}
}
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}
}
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}
}