computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...

, Programming Computable Functions (PCF), or Programming with Computable Functions, or Programming language for Computable Functions, is a

programming language A programming language is a system of notation for writing computer programs. Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...

which is typed and based on

functional programming In computer science, functional programming is a programming paradigm where programs are constructed by Function application, applying and Function composition (computer science), composing Function (computer science), functions. It is a declarat ...

, introduced by

Gordon Plotkin Gordon David Plotkin (born 9 September 1946) is a theoretical computer scientist in the School of Informatics at the University of Edinburgh. Plotkin is probably best known for his introduction of structural operational semantics (SOS) and his ...

in 1977, based on prior unpublished material by

Dana Scott Dana Stewart Scott (born October 11, 1932) is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, C ...

. It can be considered as an extended version of the

typed lambda calculus A typed lambda calculus is a typed formalism that uses the lambda symbol (\lambda) to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a ...

, or a simplified version of modern typed functional languages such as ML or

Haskell Haskell () is a general-purpose, statically typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell pioneered several programming language ...

. A

fully abstract In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called ''denotations'' ...

model for PCF was first given by

Robin Milner Arthur John Robin Gorell Milner (13 January 1934 – 20 March 2010) was a British computer scientist, and a Turing Award winner. However, since Milner's model was essentially based on the syntax of PCF it was considered less than satisfactory. The first two fully abstract models not employing syntax were formulated during the 1990s. These models are based on

game semantics Game semantics is an approach to Formal semantics (logic), formal semantics that grounds the concepts of truth or Validity (logic), validity on Game theory, game-theoretic concepts, such as the existence of a winning strategy for a player. In this ...

and Kripke logical relations. For a time it was felt that neither of these models was completely satisfactory, since they were not effectively presentable. However, Ralph Loader demonstrated that no effectively presentable fully abstract model could exist, since the question of program equivalence in the finitary fragment of PCF is not decidable.

Syntax

The ''

data type In computer science and computer programming, a data type (or simply type) is a collection or grouping of data values, usually specified by a set of possible values, a set of allowed operations on these values, and/or a representation of these ...

s'' of PCF are inductively defined as * nat is a type * For types ''σ'' and ''τ'', there is a type ''σ'' → ''τ'' A ''context'' is a list of pairs ''x : σ'', where ''x'' is a variable name and ''σ'' is a type, such that no variable name is duplicated. One then defines typing judgments of terms-in-context in the usual way for the following syntactical constructs: * Variables (if ''x : σ'' is part of a context ''Γ'', then ''Γ'' ⊢ ''x'' : ''σ'') * Application (of a term of type ''σ'' → ''τ'' to a term of type ''σ'') *

λ-abstraction In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computation based on function abstraction and application using variable binding and substitution. Untyped lambda calculus, the topic ...

* The Y fixed point combinator (making terms of type ''σ'' out of terms of type ''σ'' → ''σ'') * The successor (succ) and predecessor (pred) operations on nat and the constant 0 * The conditional if with the typing rule: :

\frac

: (nats will be interpreted as booleans here with a convention like zero denoting truth, and any other number denoting falsity)

Semantics

Denotational semantics

A relatively straightforward semantics for the language is the Scott model. In this model, * Types are interpreted as certain domains. **

!">\textbf_.html" ;"title="![ \textbf ">![ \textbf !:= \mathbb_

(the natural numbers with a bottom element adjoined, with the flat ordering) **

[\![ \sigma \to \tau \, ]\!]

is interpreted as the domain of Scott-continuous functions from

[\![\sigma]\!] \,

[\![\tau]\!] \,

, with the pointwise ordering. * A context

x_1 : \sigma_1, \; \dots, \; x_n : \sigma_n

is interpreted as the product

!">sigma_1.html" ;"title="![\sigma_1">![\sigma_1!\times \; \dots \; \times [\![\sigma_n">sigma_1">![\sigma_1<_a>!.html" ;"title="sigma_1.html" ;"title="![\sigma_1">![\sigma_1!">sigma_1.html" ;"title="![\sigma_1">![\sigma_1!\times \; \dots \; \times [\![\sigma_n!]

* Terms in context

\Gamma \; \vdash \; x \; : \; \sigma

are interpreted as continuous functions

[\![\Gamma]\!] \; \to \; [\![\sigma]\!]

** Variable terms are interpreted as projections ** Lambda abstraction and application are interpreted by making use of the

cartesian closed In category theory, a Category (mathematics), category is Cartesian closed if, roughly speaking, any morphism defined on a product (category theory), product of two Object (category theory), objects can be naturally identified with a morphism defin ...

structure of the category of domains and continuous functions ** Y is interpreted by taking the

least fixed point In order theory, a branch of mathematics, the least fixed point (lfp or LFP, sometimes also smallest fixed point) of a function from a partially ordered set ("poset" for short) to itself is the fixed point which is less than each other fixed po ...

of the argument This model is not fully abstract for PCF; but it is fully abstract for the language obtained by adding a '' parallel or'' operator to PCF.

Notes

References

* Appeared as *{{cite book , last1=Mitchell , first1=John C. , author1-link=John C. Mitchell , year=1996 , title=Foundations for Programming Languages , isbn=9780262133210 , chapter=The Language PCF , publisher=MIT Press , chapter-url=https://theory.stanford.edu/~jcm/books/fpl-chap2.ps

External links

Introduction to RealPCF

Lexer and Parser for PCF written in SML
Programming languages created in 1977 Academic programming languages Educational programming languages Functional languages Programming language theory Articles with example code