Programming Computable Functions

This is an old revision of this page, as edited by 134.157.168.58 (talk) at 14:19, 25 November 2005 (Added categories). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

The programming language Programming language for Computable Functions (or PCF for short) is a call-by-name typed functional language.


Syntax

Its types A are given by the following grammar

A ::= exp | A → A

and its terms by

M ::= x | λx:A.M | MM | n | succ M | pred M | cond M M M | YA M

where x is a variable and n an integer.

Typing rules

Semantics