Termination of a composition of terminating functions

Question

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?

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.