Programming Language Design 2

Fixed Points and Recursion in STLC

Learning Objectives

  • You know how recursion works using small step reduction
  • You know how to add a fixed point combinator to STLC

As we’ve learned on this course, recursion is one of the core elements of the functional programming paradigm. This chapter introduces some problems with recursion in STLC and then tries to fix them.

Recursion in untyped lambda calculus

In untyped lambda calculus, recursion can be implemented with the Y-combinator, πœ†π‘₯.π‘₯π‘₯

fact=(πœ†π‘₯.π‘₯π‘₯)((((πœ†π‘Ÿ.πœ†π‘›.((((if𝑛=0then1elseπ‘›β‹…π‘Ÿ π‘Ÿ(π‘›βˆ’1)⏟⏟⏟⏟⏟recursive callπ‘Ÿ π‘Ÿ=fact))))))))

Problems with typing the Y-combinator

In simply typed lambda calculus, the Y-combinator is untypable. The proof tree below shows that in order to decide upon its type, we’d have to unify ?β†’? with ?, which is impossible in the simple type system that STLC has.

VarΞ“,π‘₯::?β†’?⊒π‘₯::?β†’??Ξ“,π‘₯::?β†’?⊒π‘₯::?AppΞ“,π‘₯::?β†’?⊒π‘₯ π‘₯::?AbsΞ“βŠ’(πœ†π‘₯:?.π‘₯ π‘₯)::?

This means that doing recursion in STLC requires a different approach.

General recursion with Fixed points

You may recall the idea of fixed points from the Gleam material where you first implemented the reduce function for a language of parenthesis. After that you implemented the reduce_all function that applied reduce to the input until it found a fixed point, a point where applying reduce no longer changes the input. We can take a similar approach to help us achieve turing completeness1 in STLC.

First, let’s understand what a fixed point is.

Definition 6.8.1: Fixed Point of a FunctionGiven a type 𝐴 and a function 𝑓:𝐴→𝐴, π‘₯:𝐴 is a fixed point of 𝑓 if𝑓(π‘₯)=π‘₯.Example 6.8.2: Fixed Point of a FunctionThe following are fixed points of the respective function.‒𝑓(1)=1, where 𝑓(π‘₯)=2βˆ’π‘₯.‒𝑓(False)=False where 𝑓(𝑏:Boolean)=False.β€’False and True are both fixed points of 𝑓(𝑏:Boolean)=𝑏.β€’(πœ†π‘₯.π‘₯ π‘₯) (πœ†π‘₯.π‘₯ π‘₯)⟢(πœ†π‘₯.π‘₯ π‘₯) (πœ†π‘₯.π‘₯ π‘₯), i.e. the Y-combinator appliedto itself is a fixed point of evaluation.Example 6.8.3: Factorial as Fixed Point𝑛↦𝑛! is the fixed point offactGen(fact':β„•β†’β„•) (𝑛:β„•)≔if𝑛==0then1else𝑛⋅fact'(π‘›βˆ’1)Proof:Calling factGen with the factorial function 𝑛↦𝑛! β€œreduces” to thefollowing term:(𝑛:β„•)↦if𝑛==0then1else𝑛⋅(π‘›βˆ’1)!We have that 1=0! and 𝑛⋅(π‘›βˆ’1)!=𝑛!, so if we replace equals byequals, we get(𝑛:β„•)↦if𝑛==0then0!else𝑛!As 𝑛 is zero in the first branch, 0!=𝑛!, and we can remove theunnecessary if-then-else(𝑛:β„•)↦𝑛!Which is the factorial function by definition. Therefore the factorialfunction is the fixed point of factGen. β–‘

There are various algorithms for computing the fixed point of a function2. Due to the nature of 𝛽-reduction, the following is a natural choice for functions in the simply typed lambda calculus.

We want to find the fixed point of the STLC term 𝑓::𝑇→𝑇. The fixed point is a value π‘₯, such that 𝑓π‘₯=π‘₯3.

Note that we have to consider terms which are not abstractions, but have type 𝑇→𝑇, i.e. they can be reduced to an abstraction. Small-step semantics is key in the following algorithm for finding the fixed point of 𝑓:

  1. If 𝑓 is an abstraction πœ†π‘₯:𝑇,𝑑
    1. Return [π‘₯↦fix𝑓]𝑑 i.e. β€œcall” 𝑓 with the β€œmagic” term fix𝑓.
  2. If not
    1. Reduce 𝑓 by one step.

The β€œmagic” term fix𝑓 has to be a new term which has the above dynamics.

Let’s run an example with the fibonacci function.

First, we need to define a generating function for it. The generating function, fibGen, takes in an argument fib and returns the following function

πœ†π‘›:Integer.if𝑛<1then𝑛elsefib(π‘›βˆ’1)+fib(π‘›βˆ’2)

The whole generating function can be written as

fibGenβ‰”πœ†fib:Integerβ†’Integer.πœ†π‘›:Integer.if𝑛≀1then𝑛elsefib(π‘›βˆ’1)+fib(π‘›βˆ’2)

Now, let’s use the above algorithm to find fibGenβ€˜s fixed point fixfibGen.

We notice that fibGen is an abstraction, so we replace every occurrence of fib with fixfibGen

fixfibGen=πœ†π‘›:Integer.if𝑛≀1then𝑛elsefixfibGen(π‘›βˆ’1)+fixfibGen(π‘›βˆ’2)

If we wanted to continue the process, we could replace fixfibGen inside the abstraction with the above term, but that is not necessary until applying the abstraction.

Think about what would happen if is_value was defined such that an abstraction is a value only if its body is a value. If we kept replacing fixfibGen inside the abstraction with the above term, we would have to do it for infinitely long and would end up with an infinitely long term which would theoretically have the same behavior as the fibonacci function.

Let’s see what happens if we apply fixfibGen to the number 3.

fixfibGen3β†’β†’β†’β†’β†’β†’β†’AppAbs[𝑛↦3]if𝑛<1then𝑛elsefixfibGen(π‘›βˆ’1)+fixfibGen(π‘›βˆ’2)≑if3<1then3elsefixfibGen(3βˆ’1)+fixfibGen(3βˆ’2)β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’Ite∘LtFalseifFalsethen3elsefixfibGen(3βˆ’1)+fixfibGen(3βˆ’2)
Composition of Inference Rules

In the previous evaluation example, the reduction steps with ∘ in them have some kind of an β€œinner” reduction that happens. For example, the Ite∘EqFalse step, which reduced the condition 3<1 to False should be interpreted as pre-composing4 Ite with EqFalse.

Here are the inference rules in question:

𝑑1βŸΆπ‘‘β€²1Iteif𝑑1then𝑑2else𝑑3⟢if𝑑′1then𝑑2else𝑑3Β¬(𝑣1<𝑣2)LtFalse𝑣1<𝑣2⟢False

The composition is done by first refining the metavariable 𝑑1 to be 𝑣1<𝑣2, which changes the hypothesis to Ite to be 𝑣1<𝑣2βŸΆπ‘‘β€²1. Pre-composing the Ite rule with the LtFalse rule means that the conclusion of LtFalse is used to fill the hypothesis to Ite. In the end, we get the following partial evaluation tree:

Β¬(𝑣1<𝑣2)LtFalse𝑣1<𝑣2⟢FalseIteif𝑣1<𝑣2then𝑑2else𝑑3⟢ifFalsethen𝑑2else𝑑3

From which we can hide the internal implementation details (the function’s body if you wish) to compress it down to:

Β¬(𝑣1<𝑣2)Ite∘LtFalseif𝑣1<𝑣2then𝑑2else𝑑3⟢ifFalsethen𝑑2else𝑑3

We used this rule in the β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’Ite∘LtFalse step knowing that Β¬(3<1).

Next, let’s actually define the fix construction on top of simply typed lambda calculus (with integers and booleans).

STLC+β„•+𝟚+pairs+lists+sums+fix

Let’s define a new term Fix(t) that computes the fixed point of t using the algorithm described above. We add the term constructor into the ADT:

Term≔…|Fix(Term)

Which is equivalent with the formation rule:

𝑑:TermFixfix𝑑:Term

The notation fix𝑑 is used to informally refer to Fix(𝑑).

Dynamics for Fix

Just like with other terms that have inner subterms, we usually want to reduce the inner term inside the fix if it’s not already a value β€” call this rule Fix1. The fix-point algorithm is then encoded into the Fix2 rule and enables general recursion in STLC.

π‘‘βŸΆπ‘‘β€²Fix1fixπ‘‘βŸΆfix𝑑′Fix2fix(πœ†π‘₯:𝑇,𝑑)⟢[π‘₯↦fix(πœ†π‘₯:𝑇,𝑑)]𝑑

Let’s see how a factorial function in STLC is defined using fix.

fact≔fix πœ†fact':Integerβ†’Integer. πœ†π‘›:Integer. if𝑛==0then1else𝑛⋅fact'(π‘›βˆ’1)

As an example, let’s evaluate fact2.

First, note that

factβ†’Fix2[fact'↦fact]πœ†π‘›:𝐼.if𝑛==0then1else𝑛⋅fact'(π‘›βˆ’1)β‰‘πœ†π‘›:𝐼.if𝑛==0then1else𝑛⋅fact(π‘›βˆ’1)

Therefore App1∘Fix2 reduces the left-hand-side of the application as above, and then substitutes in [𝑛↦2].

fact2β†’β†’β†’β†’β†’β†’β†’β†’App1∘Fix2(πœ†π‘›:𝐼.if𝑛==0then1else𝑛⋅fact(π‘›βˆ’1)) 2β†’β†’β†’β†’β†’AppAbs[𝑛↦2]if𝑛==0then1else𝑛⋅fact(π‘›βˆ’1)≑if2==0then1else2β‹…fact(2βˆ’1)

Then, evaluation continues by reducing the subject of the if-then-else, followed by

β†’β†’β†’β†’β†’β†’β†’β†’Ite∘EqFalseifFalsethen1else2β‹…fact(2βˆ’1)β†’β†’β†’β†’β†’IteFalse2β‹…fact(2βˆ’1)β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’Mul2∘Fix1∘Sub2β‹…fact1β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’Mul2∘App1∘Fix22β‹…(πœ†π‘›:𝐼.if𝑛==0then1else𝑛⋅fact(π‘›βˆ’1)) 1β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’Mul2∘AppAbs2β‹…[𝑛↦1]if𝑛==0then1else𝑛⋅fact(π‘›βˆ’1)β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’Mul2∘Ite∘EqFalse2β‹…ifFalsethen1else1β‹…fact(1βˆ’1)β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’Mul2∘IteFalse2β‹…1β‹…fact(1βˆ’1)β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’Mul2∘Mul2∘Fix1∘Sub2β‹…1β‹…fact0β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’Mul2∘Mul2∘App1∘Fix22β‹…1β‹…(πœ†π‘›:𝐼.if𝑛==0then1else𝑛⋅fact(π‘›βˆ’1)) 0β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’Mul2∘Mul2∘AppAbs2β‹…1β‹…[𝑛↦0]if0==𝑛then1else𝑛⋅fact(0βˆ’1)β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’Mul2∘Mul2∘Ite∘EqTrue2β‹…1β‹…(ifTruethen1else0β‹…fact(0βˆ’1))β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’β†’Mul2∘Mul2∘IteTrue2β‹…1β‹…1β†’Mul2β‹…1β†’Mul2

For reference, here are the rules used in the above reduction:

𝑑1βŸΆπ‘‘β€²1Iteif𝑑1then𝑑2else𝑑3⟢if𝑑′1then𝑑2else𝑑3IteTrueifTruethen𝑑2else𝑑3βŸΆπ‘‘2𝑑1βŸΆπ‘‘β€²1App1𝑑1𝑑2βŸΆπ‘‘β€²1𝑑2is_value(𝑣2)AppAbs(πœ†π‘₯.𝑑1) 𝑣2⟢[π‘₯↦𝑣2]𝑑1𝑣1==𝑣2EqTrue𝑣1==𝑣2⟢Trueπ‘‘βŸΆπ‘‘β€²Fix1fixπ‘‘βŸΆfix𝑑′IteFalseifFalsethen𝑑2else𝑑3βŸΆπ‘‘3𝑑2βŸΆπ‘‘β€²2Mul2𝑑1⋅𝑑2βŸΆπ‘‘1⋅𝑑′2MulInt(𝑛1)β‹…Int(𝑛2)⟢Int(𝑛1⋅𝑛2)SubInt(𝑛1)βˆ’Int(𝑛2)⟢Int(𝑛1βˆ’π‘›2)Β¬(𝑣1==𝑣2)EqFalse𝑣1==𝑣2⟢FalseFix2fix(πœ†π‘₯:𝑇,𝑑)⟢[π‘₯↦fix(πœ†π‘₯:𝑇,𝑑)]𝑑

Statics for Fix

From Definition 6.8.1, it’s easy to derive the typing rule for fix.

If 𝑑 is a term with type 𝑇→𝑇, then fix𝑑::𝑇.

Ξ“βŠ’π‘‘::𝑇→𝑇FixΞ“βŠ’fix𝑑::𝑇
Loading Exercise...
Loading Exercise...

Designing Recursive Functions in STLC+β„•+𝟚+fix

We can use Fix to implement recursion by passing it a function that β€œtakes itself” as the first argument. This general pattern can be applied to previous knowledge of recursive functions.

The following β€œdeclaration” of the recursive function 𝑓:

𝑓:Integerβ†’Integer𝑓 π‘₯=𝑑where𝑑uses f recursively

can be turned into a term in STLC+β„•+𝟚+fix like this:

fix(πœ†π‘“:Integerβ†’Integer.πœ†π‘₯:Integer.𝑑)where𝑑uses f recursively

We will define a simple declaration and module system in the next chapter.

Problems with our approach β€” Bottom type and infinite recursion

The main problem with infinite recursion is that it breaks a crucial property of lambda calculuss, the progress theorem. This problem/tradeoff is present with most functional programming languages, as recursion is such a useful feature.

In our case if we were to, for example, pass the fact function a negative integer, the reduction of that statement would never result in a value. This would mean that the progress theorem, i.e. reducing a term will eventually produce a value, doesn’t hold.

In addition, infinite recursion can be used to produce a term of the bottom type (βŠ₯), which is sometimes called the Void type5.

Ξ“,π‘₯::βŠ₯⊒π‘₯::βŠ₯AbsΞ“βŠ’πœ†π‘₯:βŠ₯.π‘₯::βŠ₯β†’βŠ₯FixΞ“βŠ’fixπœ†π‘₯:βŠ₯.π‘₯::βŠ₯
Bottom Type

The bottom type as an ADT looks like the following

βŠ₯β‰”βŠΉ

⊹ is used to indicate the void, nothingness, or a hole puncture in the space of terms.

In Rust, as there is no way to make a tuple of zero terms, one writes

enum Bot {}

for the bottom type ADT. In Rust, the bottom type is called never.

Statics for Bottom

The bottom type has no introduction rules (ways to create an element) as it is a product (or sum) type of 0 types. The only rule is the elimination rule, which describes how one can destructure (do case matching) elements of it.

We simply add a new term absurd𝑑 (sometimes called abort, too)

Ξ“βŠ’π‘‘::βŠ₯AbsurdΞ“βŠ’absurd(𝑑)::𝑇

This rule says that a term of type βŠ₯ can always be converted to any type using absurd.

Think about why the bottom type might be useful to have in a programming language. Feel free to add the bottom type into your STLC implementation.

This problem makes the language completely useless at being used for mathematics or logic, because every statement and its negation can be proved using the above. Stronger programming languages, like proof assistants, must ensure that the bottom type is empty, i.e. has no terms. This means that in such languages general recursion is forbidden, and termination of recursion has to be proven by the programmer.

Loading Exercise...
Loading Exercise...

Footnotes

Footnotes

  1. STLC with fixed points is turing complete. Read more on StackExchange. ↩

  2. See this WikiPedia article. ↩

  3. This equality loosely speaking refers to the equality defined by 𝛽-reduction. E.g. if 𝑓π‘₯ evaluates to π‘₯ in some number of steps, then they are equal. ↩

  4. This probably sounds a lot like function composition, which is absolutely the right intuition β€” inference rules are just functions between logical propositions. ↩

  5. Some languages use the type void to mean β€œno return value”, which is in fact the unit type, also known as the top type. This is quite confusing as bottom and top types are polar opposites. ↩

← Extensions to STLC
STLC Declarations, Modules and Imports →