递归程序

问题如下。我们需要给予程序如阶乘函数的定义以语义function factorial(n:Nat):Nat ≡ if (n==0)then 1 else n*factorial(n-1)。 这个阶乘程序的意义应当是在自然数上一个函数，但是由于它的递归定义，如何以复合方式理解它是不明白的。