lambda

package
v1.3.1 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Nov 7, 2018 License: GPL-3.0 Imports: 3 Imported by: 0

README

lambda

This page gives an overview of the library on which the cLC is build.

All functions in this library work upon lambda.Terms which is an interface covering a few other datatypes. More detail is provided later on. However for most applications it's easier to use the serialization format instead of the internal representation.

Serialization

The library has a serialization format to provide an easier way to start using the library (the internal representation is rather strict).

It's basically De Bruijn index notation using l instead of λ and with free variables prefixed by ' and separated by a space or brackets. For example for the lambda expression (λx.(λy.x) x) v w you use: (l(l2)1)'v 'w.

There are two functions defined for this format:

  • Deserialize(string) (Term, error)

Turns the De Bruijn index notation into the internal representation.

  • MustDeserialize(string) Term

Same as above but panics on error.

Functions defined on Terms

  • AlphaEquivalent(Term) bool

Checks if self and the parameter are syntactically equal.

  • String() string

Returns the object as a string.

  • Serialize() string

Returns the object in the serialized format.

  • Reduce() (Term, error)

Reduces the object using the fastest method available (currently AorReduce()).

  • AorReduce() (Term, error)

Reduces the object using applicative order reduction.

  • NorReduce() (Term, error)

Reduces the object using normal order reduction.

  • WHNF() Abst

Transforms the object to a weak head normal form (usually by applying the inverse of η-reduction).

  • EtaReduce() Term

If there is eta-reduction is possible returns the object after this reduction, else return the object itself.

  • (Only defined on Abst) BetaReduce(sub Term) Term

Substitutes the locally bound variable of the Abst by sub.

Variables

  • var MaxReductions = 10000

Defines the maximum amount of reductions that are tried by the library before returning an error (useful when, for example, you try to expand the Y combinator).

If set to a negative value it will keep on expanding indefinitely.

Data types

If you need simple input of lambda expressions, look at the serialization format.

lambda contains three datatypes and one interface to represent lambda terms:

  • Term (interface) is implemented by all three data types.
  • Appl ([2]Term) represents an application.
  • Abst ([1]Term) represents a lambda abstraction.
  • Var (uint) is the De Bruijn index of a variable minus one.
  • Free (string) is the name of a free variable.

Thus as an example, the lambda term (λx.(λy.x) x) v w becomes:

Appl{
    Appl{
        Abst{
            Appl{
                Abst{
                    Var(1),
                },
                Var(0),
            },
        },
        Free("v"),
    },
    Free("w"),
}

As you can see this entire structure is a Term.

Documentation

Index

Constants

This section is empty.

Variables

View Source 
var MaxReductions = 10000

MaxReductions determines the maximum amount of expansions before we give up use a negative value to have no limit (use with care...)

Functions

func ConcAorReduce 

func ConcAorReduce(term Term, out chan Term, done chan bool)

ConcAorReduce reduces a lambda expression using applicative order, ignores MaxReductions, instead stops calculations once a signal is sent to done. If stopped mids computation puts nil on out channel.

func ConcNorReduce 

func ConcNorReduce(term Term, out chan Term, done chan bool)

ConcNorReduce reduces a lambda expression using normal order, ignores MaxReductions, instead stops calculations once a signal is sent to done. If stopped mids computation puts nil on out channel.

Types

type Abst 

type Abst [1]Term

Abst represents a lambda abstraction

func (Abst) AlphaEquivalent 

func (la Abst) AlphaEquivalent(other Term) bool

AlphaEquivalent checks whether a Abst and a Term are identical

func (Abst) AorReduce 

func (la Abst) AorReduce() (Term, error)

AorReduce reduces a lambda abstraction using applicative order

func (Abst) BetaReduce 

func (la Abst) BetaReduce(sub Term) Term

BetaReduce substitutes the localy bound variable of the Abst by sub

func (Abst) Copy 

func (la Abst) Copy() Term

Copy creates a copy of the abstraction

func (Abst) EtaReduce 

func (la Abst) EtaReduce() Term

EtaReduce applies eta-reduction to the Abst when possible

func (Abst) NorReduce 

func (la Abst) NorReduce() (Term, error)

NorReduce reduces a lambda abstraction using normal order

func (Abst) Reduce 

func (la Abst) Reduce() (Term, error)

Reduce reduces a lambda abstraction using applicative order

func (Abst) Serialize 

func (la Abst) Serialize() string

Serialize returns the lambda abstraction as a De Bruijn index representation

func (Abst) String 

func (la Abst) String() string

String returns the lambda abstraction as a string

func (Abst) WHNF 

func (la Abst) WHNF() Abst

WHNF returns the abstraction

type Appl 

type Appl [2]Term

Appl represents an application

func (Appl) AlphaEquivalent 

func (lx Appl) AlphaEquivalent(other Term) bool

AlphaEquivalent checks whether the Appl is identical to a Term

func (Appl) AorReduce 

func (lx Appl) AorReduce() (Term, error)

AorReduce reduces an application using applicative order

func (Appl) Copy 

func (lx Appl) Copy() Term

Copy creates a copy of the application

func (Appl) EtaReduce 

func (lx Appl) EtaReduce() Term

EtaReduce applies eta-reduction to the Appl when possible

func (Appl) NorReduce 

func (lx Appl) NorReduce() (Term, error)

NorReduce reduces an application using normal order

func (Appl) Reduce 

func (lx Appl) Reduce() (Term, error)

Reduce reduces an application using applicative order

func (Appl) Serialize 

func (lx Appl) Serialize() string

Serialize returns the application as a De Bruijn index representation

func (Appl) String 

func (lx Appl) String() string

String returns the Lambda Expression as a string

func (Appl) WHNF 

func (lx Appl) WHNF() Abst

WHNF encapsulates the expression in a lambda abstraction

type Free 

type Free string

Free is a free variable

func (Free) AlphaEquivalent 

func (lf Free) AlphaEquivalent(other Term) bool

AlphaEquivalent checks whether a Free and a Term are identical

func (Free) AorReduce 

func (lf Free) AorReduce() (Term, error)

AorReduce returns the variable itself

func (Free) Copy 

func (lf Free) Copy() Term

Copy returns the value of the free variable

func (Free) EtaReduce 

func (lf Free) EtaReduce() Term

EtaReduce returns the variable

func (Free) NorReduce 

func (lf Free) NorReduce() (Term, error)

NorReduce returns the variable itself

func (Free) Reduce 

func (lf Free) Reduce() (Term, error)

Reduce returns the variable itself

func (Free) Serialize 

func (lf Free) Serialize() string

Serialize the free varaible as ' (prime) followed by the variable name

func (Free) String 

func (lf Free) String() string

String returns the lambda variable as a string

func (Free) WHNF 

func (lf Free) WHNF() Abst

WHNF encapsulates the free variable inside of a lambda abstraction

type Term 

type Term interface {
	AlphaEquivalent(Term) bool
	EtaReduce() Term

	String() string

	Reduce() (Term, error)
	NorReduce() (Term, error)
	AorReduce() (Term, error)

	WHNF() Abst

	Copy() Term

	Serialize() string
	// contains filtered or unexported methods
}

Term is a general type to represent both Applns, Absts, Vars and Frees

func Deserialize 

func Deserialize(inpt string) (Term, error)

Deserialize turns a De Bruijn index representation into the internal representation

func MustDeserialize 

func MustDeserialize(inpt string) Term

MustDeserialize turns a De Bruijn index representation into the internal representation, panics on error

type Var 

type Var uint

Var is the De Bruijn index of a bound variable minus one

func (Var) AlphaEquivalent 

func (lv Var) AlphaEquivalent(other Term) bool

AlphaEquivalent checks whether a Var and a Term are identical

func (Var) AorReduce 

func (lv Var) AorReduce() (Term, error)

AorReduce returns the variable itself

func (Var) Copy 

func (lv Var) Copy() Term

Copy returns the value of the variable

func (Var) EtaReduce 

func (lv Var) EtaReduce() Term

EtaReduce returns the variable

func (Var) NorReduce 

func (lv Var) NorReduce() (Term, error)

NorReduce returns the variable itself

func (Var) Reduce 

func (lv Var) Reduce() (Term, error)

Reduce returns the variable itself

func (Var) Serialize 

func (lv Var) Serialize() string

Serialize returns the variable as a De Bruijn index representation

func (Var) String 

func (lv Var) String() string

String returns the lambda variable as a string

func (Var) WHNF 

func (lv Var) WHNF() Abst

WHNF encapsulates the Lambda variable inside of a lambda abstraction

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.