PCF

Programming Computable Functions

Haskell implementation of Gordon Plotkin's typed lambda calculus. It has a base type Nat, the function type T->T, Succ \ Predessors on Nats, and general recursion on Nats through use of a Y combinator. It is Turing Complete, but not strongly normalizing for all terms.

PCF is considered to be a simplified version of modern functional languages such as Haskell; where non-nonsensical terms are prohibited by the type system but recursion is afforded by Y.

Prerequisites

You need Haskell, this compiles with GHC 8.2.2 at least (Stack resolver: lts-11.0).

Optional: If you want to run the tests for this module, you'll need QuickCheck.

To Build & Run

You can use cabal to build and run this, see this README, alternatively you can use vanilla ghc to build:

To compile and run do: ghc -O2 -o pcf Main then run ./pcf

Alternatively to use the GHCi Interpreter do: ghci Main then type main

In either case you get something like the following:

Welcome to the PCF REPL
Type some terms or press Enter to leave.
>

Note: When run in GHCi, you don't have the luxury of escaped characters, backspace, delete etc... Compile it using GHC if you need this.

Examples

Where you can then have some fun, try these examples:

• \x:Nat.x
• p (s z) this is pred of succ of zero, or zero.
• s (s z) this is two
• Y (\f:Nat -> Nat.\x:Nat.if x z (if (p x) (s z) (f (p (p x))))) (p (p z))

The parser is also smart enough to recognise λ, so you can copy and paste from the output:

>   \x:Nat.x
=   λx:Nat.x
>   λx:Nat.x
=   λx:Nat.x

> denotes the REPL waiting for input, = means no reductions occurred (it's the same term), ~> denotes one reduction, and ~>* denotes 0 or more reductions (although in practice this is 1 or more due to =).

There is also a reduction tracer, which should print each reduction step. prefix any string with ' in order to see the reductions:

>   'Y (\f:Nat -> Nat.\x:Nat.if x z (if (p x) (s z) (f (p (p x))))) (p (p z))
~>  (λx:Nat.if x z (if (p x) (s z) (Y (λf:Nat->Nat.λx:Nat.if x z (if (p x) (s z) (f (p (p x))))) (p (p x))))) (p (p z))
~>  if (p (p z)) z (if (p (p (p z))) (s z) (Y (λf:Nat->Nat.λx:Nat.if x z (if (p x) (s z) (f (p (p x))))) (p (p (p (p z))))))
~>  if (p z) z (if (p (p (p z))) (s z) (Y (λf:Nat->Nat.λx:Nat.if x z (if (p x) (s z) (f (p (p x))))) (p (p (p (p z))))))
~>  if z z (if (p (p (p z))) (s z) (Y (λf:Nat->Nat.λx:Nat.if x z (if (p x) (s z) (f (p (p x))))) (p (p (p (p z))))))
~>  z

Note: the above is a function to check if 2 is even. z is considered true.

There is also a typing mechanism, which should display the type or fail as usual.

>   t(\x:Nat.\y:Nat. x) z (s z)
Nat
>   t(\x:Nat. x x)
Cannot Type Term: (\x:Nat. x x)

Note: if you provide a non-normalizing term (without Y), the type checker will fail and reduction will not occur.

Termination is not guaranteed if you misuse Y, just like in ULC.

You can save variables for the life of the program with a let expression. Any time a saved variable appears in a term, it will be substituted for the saved term:

>   let one = s z
Saved: s z
>   let plusone = \n:Nat.s n
Saved: λn:Nat.s n
>   plusone one
~>* s (s z)

Note: Consequently let and = are keywords, and so you cannot name variables with these. Additionally Nat, z, s, p, if, and Y are keywords in PCF.

Syntax

We base the language on the BNF for PCF:

However we adopt standard bracketing conventions to eliminate ambiguity in the parser. Concretely, the parser implements the non-ambiguous grammar as follows:

Some notes about the syntax:

• The above syntax only covers the core calculus, and not the repl extensions (such as let bindings above). The extensions are simply added on in the repl.
• Variables are strings (excluding numbers), as this is isomorphic to a whiteboard treatment and hence the most familiar.
• Types are either literal Nat base types or nested arrow types: T -> T. Arrows associate to the right so that Nat -> Nat -> Nat is the same as Nat -> (Nat -> Nat) but not ((Nat -> Nat) -> Nat).
• Nested terms don't need brackets: \x:Nat.\y:Nat. y unless enforcing application on the right. Whitespace does not matter (\x:Nat. x) unless it is between application where you need at least one space.
• We consider p z = z as this language has no error mechanism.
• Y is the fabled Y combinator, use it to get general recursion.
• To quit use Ctrl+C or whatever your machine uses to interrupt computations.

Semantics

The semantics implements beta-reduction on terms and alpha-equivalence as the Eq instance of PCFTerm. The semantics are the same as the STLC but with additional rules for if, zero, pred, succ, and Y. We reformulate the semantics as typing judgements:

for variables

for abstractions:

and application:

the reduction relation is adopted from STLC:

for zero, pred, and succ:

for if statements:

and there are special elimination and reduction rules for general recursion:

or in other words:

• This implementation follows a small-step operational semantics and Berendregt's variable convention (see substitution in PCF.hs).
• Reductions include the one-step reduction (see reduce1 in PCF.hs), the many-step reduction (see reduce in PCF.hs).

Other Implementation Details

• PCF.hs contains the Haskell implementation of the calculus, including substitution, reduction, and other useful things.
• Parser.hs contains the monadic parser combinators needed to parse input strings into typed-term ASTs for the calculus.
• Repl.hs contains a simple read-eval-print loop which hooks into main, and into the parser.
• Main.hs is needed for GHC to compile without any flags, it also invokes the repl.
• Tests.hs is the test suite. We have unit tests for terms in the language. QuickCheck is used to generate arbitrary trees and test they are parsed and printed correctly.

For contributions, see the project to-do list or submit a PR with something you think it needs.