Skip to content

Latest commit

 

History

History
155 lines (106 loc) · 14.7 KB

README.md

File metadata and controls

155 lines (106 loc) · 14.7 KB
Raw

System T

Haskell implementation on Kurt Godel's typed lambda calculus. It has a base type Nat, Successors on Nats, the function type T->T, and primitive recursion on Nats. It is strongly normalizing, but not Turing Complete.

Godel used this language to prove the consistency of arithmetic.

Prerequisites

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

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 st Main.hs then run ./st

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

In either case you get something like the following:

Welcome to the System T 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
  • s (s z)

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

Welcome to the System T REPL
Type some terms or press Enter to leave.
>   \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:

>   '(λa:Nat.λb:Nat.rec (λc:Nat.λd:Nat.s d) a b) z (s z)
~>  (λb:Nat.rec (λc:Nat.λd:Nat.s d) z b) (s z)
~>  rec (λc:Nat.λd:Nat.s d) z (s z)
~>  (λc:Nat.λd:Nat.s d) z (rec (λc:Nat.λd:Nat.s d) z z)
~>  (λd:Nat.s d) (rec (λc:Nat.λd:Nat.s d) z z)
~>  s (rec (λc:Nat.λd:Nat.s d) z z)
~>  s z

Note: The above adds zero to one.

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

>   t(λx:Nat.λy:Nat.rec (λa:Nat.λb:Nat.s b) x y) z (s z)
Nat
>   t\x:Nat. x x
Cannot Type Term: \x:Nat. x x

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

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 plus = λa:Nat.λb:Nat.rec (λc:Nat.λd:Nat.s d) a b
Saved: λa:Nat.λb:Nat.rec (λc:Nat.λd:Nat.s d) a b
>   plus one one
~>* s (s z)

Note: Consequently let and = are keywords, and so you cannot name variables with these. Additionally z, s, and rec are keywords in System T.

Syntax

We base the language on the BNF for System T:

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. x 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.
  • 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 STTerm. The semantics are the same as the STLC but with additional rules for zero, succ, and rec. We reformulate the semantics as typing judgements:

for variables

for abstractions:

and application:

the reduction relation is adopted from STLC:

for zero and succ:

There are similar inner reduction rules for each of the inner arguments of rec however these are subsumed by beta-reduction. There are special elimination and reduction rules for primitive recursion on Nats:

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

Other Implementation Details

  • SystemT.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.

Work initially documented here.