Type level lambda calculus in Scala

This repository demonstrates an implementation of lambda calculus in Scala types.

Untyped lambda calculus

import lambda._
case class Equals[A >: B <: B, B]() // this checks type equality

type S = x ->: y ->: z ->: ( x @@ z @@ (y @@ z) )
type K = x ->: y ->: x

type result = ( S @@ K @@ K @@ a ) # ->*
Equals[result, a]

More examples are found in TermSpec.scala.

Syntax

	Code
Variables	`a`, `b`, ..., `z`
Abstraction	`v ->: M`
Application	`M @@ N`
Terms	`M`, `N`
1-step beta reduction	`M # ->`
Multi-step beta reduction	`M # ->*`

You can define your own variables by calling #next of existing (last defined) variable
```
type variableName1 = z #next
type variableName2 = variableName1 #next
```
You may need parenthesis to avoid ambiguity

Capture-avoiding substitutions

Lambda terms are converted internally to De Bruijn indexed terms and indices are shifted during substitution to ensure capture-avoiding semantics.

License

Copyright (C) INA Lintaro
MIT License

References