A (JavaScript) Pilgrimage to Lambda Calculus

t ::=
x value
λx.t abstraction
t t application
1)       t1 → t1'
—————————————————
t1 t2 → t1' t2
2) t2 → t2'
—————————————————
v1 t2 → v1 t2'
3) (λx. t3) v2 → [x ↦ v2]t3
Zero: λs.λx.x
One: λs.λx.s x
Two: λs.λx.s s x
Three: λs.λx.s s s x
.
.
.
Ten: λs.λx.s s s s s s s s s s x
const Variable = function(info, variableName, deBruijnIndex, ctx)
{
const self = getInstance(this, Variable)
self['project'] = /* defined later */ self['setDeBruijnIndex'] = (ctx) =>
{
/* defined later */
}
return Object.freeze(self)
}
const Abstraction = 
function(info, variableName, term, isParens, ctx)
{
const self = getInstance(this, Abstraction)
self[‘project’] = /* defined later */ self[‘setDeBruijnIndex’] = (ctx) =>
{
/* defined later */
}
return Object.freeze(self)
}
const Application = function(info, lhs, rhs, isParens, ctx){
const self = getInstance(this, Application)
self[‘project’] = /* defined later */ self[‘setDeBruijnIndex’] = (ctx) =>
{
/* defined later */
}
return Object.freeze(self)
}
const getInstance = (self, constructor) =>
(self instanceof constructor) ?
self :
Object.create(constructor.prototype) ;
TERM
= ABSTRACTION
/ APPLICATION
TERM_OR_VARIABLE
= L_PARENS x:TERM R_PARENS
{
return setParens(x)
}
/ VARIABLE
VARIABLE
/************************************************************
variable ::= x
************************************************************/
= x:CHARACTER
{
return Variable(location(), x)
}
APPLICATION
/************************************************************
Term | Variable -> END
************************************************************/
= x:TERM_OR_VARIABLE END
{
return x
}
/************************************************************
Term | Variable -> ?
************************************************************/
/ x:TERM_OR_VARIABLE !TERM_OR_VARIABLE
{
return x
}
/*************************************************************
Term | Variable -> Term | Variable -> … -> Term | Variable
*************************************************************/
/ terms:TERM_OR_VARIABLE*
{
return reduceTerms(location(), terms)
}
ABSTRACTION
/************************************************************
‘λ’ -> Variable -> ‘.’ -> Term
*************************************************************/
= LAMBDA x:CHARACTER DOT term:TERM
{
return Abstraction(location(), x, term, false)
}
A → A α | β
A → β A’A’ → ɛ | α A’
APP
= lhs:TERM_OR_VARIABLE rhs:APP_
{
return Application(location(), lhs, rhs, false)
}
APP_
= lhs:TERM_OR_VARIABLE rhs:APP_
{
return Application(location(), lhs, rhs, false)
}
/ lhs:TERM_OR_VARIABLE END
{
return lhs
}
END
= !.
  1. A single term
  2. A term followed by a single something else (another term)
  3. And a list of terms
terms:TERM_OR_VARIABLE*
{
return reduceTerms(location(), terms)
}
const reduceTerms = function(info, terms){
const initialLhs = terms.shift()
const initialRhs = terms.shift()
const initialApp = Application(
info,
initialLhs,
initialRhs,
false)
// reduce terms by combining via Application
const appAll = terms.reduce(
(lhs, rhs) => Application(info, lhs, rhs, false),
initialApp
)
return appAll ;
}
  1. Extract the first two terms and form an Application object which will serve as the initial instance of the reduction
  2. Reduce the following terms, where the reducing function takes the LHS as the aggregate and returns a new Application object with the RHS applying to the LHS.
Application(
Application(
Application(
T1,
T2
),
T3
),
T4
)
λx.λy.x y
λx.λx.x x
λx.λy.y y
λx.λy.0 0
λ.λ.0 0
λx.λy.1 0
λ.λ.1 0
λx.x
λy.y
λ.0
λ.0
const match = (x, o) => {     const className = x.constructor.name     /* object o has a matching type, with a project property */
if(o[className] && x[‘project’])
{
return o[className].apply(null, x[‘project’])
}
/* wildcard */
else if(o[‘_’])
{
return o[‘_’].apply(null, x[‘project’])
}
throw “Match case unhandled”
}
const Point = (x, y) =>
{
const self = getInstance(this, Application)
self[‘project’] = [x, y]
}
const p = Point(10, 15) ;match(p, { “Point”: ([x, y]) =>
console.log(`p is Point(${x}, ${y})`),
“SomeOtherType”: (_) =>
console.log(’p is SomeOtherType’),
“_”: (_) =>
console.log(’p is an unknown type’),
})
const match2 = (…xs) => {     const functionMap = xs.pop()
const getFromFunctionMap = x => functionMap[x]
const isInFunctionMap = x =>
getFromFunctionMap(x) !== undefined
const getMatchedF = S.pipe([
getTypeNamePermutations,
//=> [[T1,…TN]]
S.map(joinWithSpace),
//=> [“T1 …TN”]
S.map(trim),
//=> [“T1 …TN”]
concatUnderscore,
//=> [“T1 …TN”, “_”]
S.find(isInFunctionMap),
//=> Maybe “T1…TN”
S.map(getFromFunctionMap),
//=> Maybe (…xs -> ?)
getValue
])
const getProjections = xs =>
xs.reduce((a,x)=>{
const y = getProjection(x)
return a.concat([y])
}, [])
const matchedF = getMatchedF(xs) const args = getProjections(xs) if(matchedF)
{
return matchedF.apply(
null, (xs.length > 1) ? [args] : args[0])
}
throw “Match case unhandled”}
const p = Point(10, 15) ;match2(p, p, {

“Point Point”: ([[x, y], [x2, y2]]) =>
console.log(`Object1 is Point(${x}, ${y}) and Object2 is
Point(${x2}, ${y2})`),
“Point _”: ([[x, y], _]) =>
console.log(’Object1 is a Point(${x}, ${y}) and Object2 is
unknown’),
“_ Point”: ([_, [x, y]]) =>
console.log(’Object1 is unknown and Object2 is a
Point(${x}, ${y}) ’),
“_”: (_) =>
console.log(’they both are unknown types’),
})
  1. Evaluate the LHS first
  2. When that can no longer be reduced, evaluate the RHS
  3. When both sides are reduced to their furthest and you are left with Values perform substitution
const isValue = (ctx, term) => {      return match2(term, {          “Abstraction”: _ => true,          “_”: _ => false     })}const _eval = (ctx, ast) => match2(ast, {      “Abstraction”: _ => ast,      “Application”: (info, lhs, rhs, _) => {          // Rule 3.
if(isValue(ctx, lhs) && isValue(ctx, rhs))
{
const lhsTerm = lhs.project[2] ;
return substitue(rhs, lhsTerm)
}
// Rule 2. Eval RHS
else if(isValue(ctx, rhs))
{
return Application.cloneWithRhs(ast, _eval(ctx, rhs))
}
// Rule 1. Eval LHS
else
{
return Application.cloneWithLhs(ast, _eval(ctx, lhs))
}
},
“_”: _ => { if(isValue(ast))
{
return ast
}
else
{
throw NO_RULES_APPLY
}
}})
λx.(λy.λz.y z)(λn.x)
  1. Remove the lambda term on the LHS and rewire the LHS parent node down to the next term
  2. Replace the variable reference in the LHS with he RHS Lambda Term
  1. All abstraction below the substitution point where the the parent node is rewired need to be investigated.
  2. All variable references with a DE Bruijn Index > 0 need to have one level of reference added to it
// "shift" the deBruijnIndex all variables within AST by some amount
const substitue = (application) => {
const a = shift(-1, application) ;
const [info, lhs, rhs, _] = a ;
const lhsTerm = lhs.project[2] ;
return shift(1, _substitue(rhs, lhsTerm))
}
const _substitue = (replacement, ast) => { return match2(ast, {
"Application": (info, lhs, rhs, isParens, ctx) => {
return Application(
info,
_substitue(replacement, lhs),
_substitue(replacement, rhs),
isParens,
ctx
)
},

"Abstraction": (info, variableName, term, isParens, ctx) =>{
return Abstraction(
info,
variableName,
_substitue(replacement, term),
isParens,
ctx
)
},
"Variable": (info, variableName, deBruijnIndex, ctx) => {
if(deBruijnIndex === 0) {
return replacement ;
}
return ast ;
}
})
}
const shift = (amount, ast) => { return match2(ast, {
"Application": (info, lhs, rhs, isParens, ctx) => {
const lT = shift(amount, lhs)
const rT = shift(amount, rhs)
const a = Application(
info,
lT,
rT,
isParens,
ctx
)
return a
},
"Abstraction": (info, variableName, term, isParens, ctx) =>{
const t = shift(amount, term)
const a = Abstraction(
info,
variableName,
t,
isParens,
ctx
)
return a ;
},
"Variable": (info, variableName, deBruijnIndex, ctx) => {
const v = Variable(
info,
variableName,
deBruijnIndex + amount,
ctx
)
return v
}
})
}

--

--

--

A 25 year software industry veteran with a passion for functional programming, architecture, mentoring / team development, xp/agile and doing the right thing.

Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

Aw, Crud!

How I Failed As A Scrum Master For My Most Prestigious Team

A desperate woman with a hand in front of her face

Object Oriented Concepts in NutShell

Classifying What You’ve Learned

Optimisations and checkpointing for spark streaming job

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Todd Brown

Todd Brown

A 25 year software industry veteran with a passion for functional programming, architecture, mentoring / team development, xp/agile and doing the right thing.

More from Medium

The “Zero, One, Infinity” rule

Thinking in TypeScript: for the Eager Java Developer

An Overview of Cache & its Types