License	GPL-3
Safe Haskell	Safe

Lambda

Description

This module deals with the parsing, reduction and printing of lambda expressions using DeBruijn notation. The interpreter uses DeBruijn notation as an internal representation and as output format. This is because it is easier to do beta reduction with DeBruijn indexes.

Synopsis

Documentation

data Exp Source #

A lambda expression using DeBruijn indexes.

Constructors

Var Integer	integer indexing the variable.
Lambda Exp	lambda abstraction.
App Exp Exp	function application.
Pair Exp Exp	typed pair of expressions.
Pi1 Exp	typed first projection.
Pi2 Exp	typed second projection.
Inl Exp	typed left injection.
Inr Exp	typed right injection.
Caseof Exp Exp Exp	typed case of.
Unit	typed unit element.
Abort Exp	typed abort derivation.
Absurd Exp	typed absurd derivation.

Instances

Eq Exp Source #
Methods (==) :: Exp -> Exp -> Bool (/=) :: Exp -> Exp -> Bool
Ord Exp Source #
Methods compare :: Exp -> Exp -> Ordering (<) :: Exp -> Exp -> Bool (<=) :: Exp -> Exp -> Bool (>) :: Exp -> Exp -> Bool (>=) :: Exp -> Exp -> Bool max :: Exp -> Exp -> Exp min :: Exp -> Exp -> Exp
Show Exp Source #
Methods showsPrec :: Int -> Exp -> ShowS show :: Exp -> String showList :: [Exp] -> ShowS

simplifyAll :: Exp -> Exp Source #

Applies repeated simplification to the expression until it stabilizes and returns the final simplified expression.

>>> simplifyAll $ App (Lambda (Var 1)) (Lambda (Var 1))
λ1

simplifySteps :: Exp -> [Exp] Source #

Applies repeated simplification to the expression until it stabilizes and returns all the intermediate results.

>>> simplifySteps $ App (Lambda (Var 1)) (Lambda (Var 1))
[(λ1 λ1),λ1]

showReduction :: Exp -> String Source #

Shows an expression coloring the next reduction.

usestypecons :: Exp -> Bool Source #

Determines if the given variable is free on the expression. freein :: Integer -> Exp -> Bool freein n (Var m) = n == m freein n (Lambda e) = freein (succ n) e freein n (App u v) = (freein n u) && (freein n v)

Returns true if the expression has at least one type constructor.

isOpenExp :: Exp -> Bool Source #

Returns true if the expression contains open undefined variables.