Suppose there are two functions:

$ f : X \rightarrow Y $ and $g : Y \rightarrow Z$

Both $g$ and $f$ can be implemented as algorithms that yield the correct result in a finite amount of time.

It appears to be obvious, that there is also a correct and terminating algorithm that computes the composition of the two $g \circ f$.

But why is that so? Do I need to argue that for both functions, there is a representation in the lambda calculus and in that calculus (with a small-step semantics), there is a trivial implementation of $\circ$? Doesn't that require an encoding of $X$,$Y$ and $Z$? Is there a more fundamental theorem?


1 Answer 1


Indeed this is obvious. Now you need to "prove" it. The difficulty will depend on what definitions (and axioms) you assume when you say that "$f$ and $g$ can be implemented". Start by making these definitions explicit.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.