---
tags:
  - lecture-note/unprocessed
  - 31-14/COMSM0067
---
Recursion breaks termination:
![](2025-10-21%20Recursion%202025-10-21%2011.02.02.excalidraw.svg)
%%[🖋 Edit in Excalidraw](2025-10-21%20Recursion%202025-10-21%2011.02.02.excalidraw.md)%%
# Recursion + Fixed Points
In STLC we want to preserve termination, so we'll instead create a new language for recursion: PCF. Which is (some version of) STLC + Fixed Points.
![](2025-10-21%20Recursion%202025-10-21%2011.11.30.excalidraw.svg)
%%[🖋 Edit in Excalidraw](2025-10-21%20Recursion%202025-10-21%2011.11.30.excalidraw.md)%%
# STLC vs PCF
PCF has no strings, and has partial functions instead of total functions. We also do pure natural numbers as successors of zero. We also have a function for testing for zero.
## Partial Functions
A partial function is a function that may not be defined for all inputs.
![](2025-10-21%20Recursion%202025-10-21%2011.35.25.excalidraw.svg)
%%[🖋 Edit in Excalidraw](2025-10-21%20Recursion%202025-10-21%2011.35.25.excalidraw.md)%%
# Related Reading
- [2025-10-22 Recursion 2](2025-10-22%20Recursion%202.md)