User:Cjoev/PCF

Note: This page contains some material I am drafting for addition to the article Programming language for Computable Functions. If I am creating it incorrectly and it does not end up being a user subpage of mine, please inform me. User:Cjoev

Syntax

This account of PCF is based upon that of Mitchell (1996).

There are two major syntactic classes in PCF, the terms and the types. In what follows, the letters $\sigma$ and $\tau$ will generally stand for types; the letter $e$ will stand for a term, and letters such as $x$, $y$ and $f$ will be variables. Both sets are defined inductively -- that is, each one is the smallest set satisfying certain closure rules. The abstract syntax of types is given by:

$\tau ,\sigma ::={\texttt {nat}}\ |\ {\texttt {bool}}\ |\ \sigma \times \tau \ |\ \sigma \to \tau$

and the set of terms is defined as follows:

$e::=$	$x$ $|$ 0 $|$ 1 $|$ 2 $|$ $\cdots$ $|$ true $|$ false	(variables,literals)
	$|$ $e_{1}+e_{2}$ $|$ $e_{1}=e_{2}$ $|$ if $e_{1}$ then $e_{2}$ else $e_{3}$	(addition, equality test, conditional)
	$|$ $\langle e_{1},e_{2}\rangle$ $|$ $\pi _{1}\ e$ $|$ $\pi _{2}\ e$	(pairing,projections)
	$|$ $\lambda x:\tau .e$ $|$ $e_{1}$ $e_{2}$	(abstraction, application)
	$|$ fix${}_{\tau }$	(fixed point operator)

To Be Written...

• Derived syntactic forms (let, fun, letrec) and common functions (${\mathit {pred}}$)

• Typing Rules

• Operational semantics (call-by-name vs. call-by-value)

• Examples

References

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