Data.Lambda.Model

Size notion framework of Gittenberger and Gołębiewski for lambda terms in the de Bruijn notation. A size definition constitutes the weights for lambda abstraction, term application, successor and zero.

Size notions

data Model a

Lambda term size model.

Constructors

Model

Fields

• zeroW :: a

  Size of zero

• succW :: a

  Size of successor

• absW :: a

  Size of the abstraction

• appW :: a

  Size of the application

natural :: Integral a => Model a

The natural size notion.

binary :: Integral a => Model a

The binary size notion.

valid

Arguments

:: Integral a

=> Model a

Size notion

-> Bool

Whether the size model is valid.

Checks whether the given size model is valid in the framework of Gittenberger and Gołębiewski.

Helpers

weights :: Model a -> (a, a, a, a)

Given a size notion, returns a tuple (a,b,c,d) where a denotes the size of the de Bruijn zero, b denotes the size of the de Bruijn successor, c denotes the size of the lambda abstraction and finally d denotes the size of the application.