lambda-sampler-1.0: Boltzmann sampler utilities for lambda calculus.

Copyright(c) Maciej Bendkowski 2016
LicenseBSD3
Maintainermaciej.bendkowski@tcs.uj.edu.pl
Stabilityexperimental
Safe HaskellSafe
LanguageHaskell2010

Data.Lambda

Contents

Description

Lambda terms in the de Bruijn notation where instead of variables, we use natural indices encoded as a sequence of successors of zero.

Each index captures the distance to its binding lambda - Z corresponds to a variable bound by the first lambda abstraction on its way to the term root. The successor S increases the distance of its argument by one. If an index points to a lambda abstraction outside of the term, then that index represents a free variable in the term. Such a representation for lambda terms avoids using explicit variable names and hence eliminates the use of alpha-conversion.

Synopsis

Lambda terms

data Lambda Source #

Lambda terms with de Bruijn indices.

Constructors

Var Index

de Bruijn indices.

Abs Lambda

Lambda abstraction.

App Lambda Lambda

Term application.

Instances

isClosed :: Lambda -> Bool Source #

Predicate defining closed lambda terms.

size Source #

Arguments

:: Num a 
=> Model a

Size notion used in the computations.

-> Lambda

The considered lambda term.

-> a

The integer size of the lambda term.

Computes the size of the given lambda term.

sizeVar Source #

Arguments

:: Num a 
=> Model a

Size notion used in the computations.

-> Index

The considered de Bruijn index.

-> a

The integer size of the lambda term.

Computes the size of the given de Bruijn index.

maxIndex :: (Num a, Ord a) => Lambda -> a Source #

Finds the maximal index in the given lambda term.

de Bruijn indices

data Index Source #

de Bruijn indices in unary notation.

Constructors

S Index 
Z 

Instances

toInt :: Num a => Index -> a Source #

Translates the given index to a corresponding positive integer.

toIndex :: (Num a, Eq a) => a -> Index Source #

Translates the given positive integer to a corresponding index.