Skip to content

Latest commit

 

History

History
93 lines (57 loc) · 2.49 KB

README.md

File metadata and controls

93 lines (57 loc) · 2.49 KB

The Jebus Lambda Calculus Interpreter

Jebus is an interpreter for a lambda calculus variation implemented in Haskell. Jebus was created for demonstration purposes, as part of a lambda calculus course of National Technical University of Athens.

Syntax

e ::= e1 e2
| """ ident "." e
| "let" ["rec"] ident "=" e1 "in" e2
| "["e1"," e1"]"
| "true" | "false"
| "if" e1 "then" e2 "else" e3
| e1 op e2
| e1 rop e2
| e1 bop e2

op ::= "+" | "-" | "*" | "**"

rop ::= "=" | "<" | "<=" | ">" | ">="

bop ::= "&&" | "||"

Typing

The language is strictly typed using the Hindley–Milner type system. The types are implicit in the source and they are reconstructed before the interpretation using the algorithm W for type inference. The supported types are natural numbers, booleans, function and product types. It features let-polymorphism.

Built-in Functions

The implementation also provides the following build-in functions:

  • succ : nat -> nat
  • pred : nat -> nat
  • iszero : nat -> bool
  • not : bool -> bool
  • fst : a x b -> a
  • snd : a x b -> b

Usage

To compile:

$ gch jebus.hs

Jebus reads a program from the standard input. The following command-line options are available:

$ jebus [COMMAND] ... [OPTIONS]

Common flags:
	-h --help           Display help message
	-V --version        Print version information

jebus annot 
	Prints an explicitly typed version of the program

jebus eval [OPTIONS]
	Interpret the program

	-t --trace          show each beta reduction
	-e --eval=EVALMODE  specify evaluation strategy: normal (default) or
    	                applicative

Dependencies

Implementation

All the functionality is implemented using abstractions and function applications. For more imformation about the implementation read the slides in the report directory.