非递归lambda calculus析因函数 [英] non recursive lambda calculus factorial function

问题描述

如何在不使用lambda演算递归的情况下编写阶乘函数？意味着数学符号不能在任何特定的编程语言中实现。

解决方案

如果使用不使用递归，则表示没有一般递归和
，因此没有固定点应用程序），我们可以简单地观察到阶乘函数是原始递归的（即本质上是迭代的），并且通过迭代（由教会数字提供）和对，存在非常普遍和简单的原始递归编码。
我会讨论这个非常具有启发性的一般情况。
让< M，N>是对的一些编码，并且让fst和snd是关联的
投影。例如，您可以定义

 < M，N> =λz。 z M N 
 fst =λp。 p（λxy.x）
 snd =λp。 p（λxy.y）
  

假设有一个原始的递归定义（不带参数
为简单起见）

  f（0）= a 
f（x + 1）= h（x， f（x））
  

其中a和h已经被定义。 b

总的想法是使用辅助函数f'，其中

  f'（x） =< x，f（x）> 
  

因此，f'（0）=< 0，a>，并且给定对p =< x，f（x）> = f'（x），我们建立
下一对<通过计算第一个分量
的后继和将h应用于这对参数（即利用我们的
编码对），简单地等于通过x + 1，f（x + 1）继续h作为对p的输入）。

  next =λp。< succ（fst p），p h> 
  

最后，为了计算f（n），我们需要迭代n次函数next
从< 0，a>，然后取第二个组件：

  f =λn。 snd（n next <0，a>）
  

How to write a factorial function without use of recursion using lambda calculus? Meaning just the math notation not implementation in any particular programming language.

解决方案

If by "without the use of recursion" you mean without general recursion and hence without fixpoints (or self applications), we can simply observe that the factorial function is primitive recursive (that is, iterative, in essence), and there is a very general and simple encoding of primitive recursion by means of iteration (provided by church numerals) and pairs. I will discuss the general case that is quite instructive. Let < M,N > be some encoding of pairs, and let fst and snd be the associated projections. For instance, you can define

<M,N> = λz. z M N
fst = λp. p (λxy.x)
snd = λp. p (λxy.y)

Suppose to have a primitive recursive definition (without parameters, for the sake of simplicity)

f(0) = a
f(x+1) = h(x,f(x))

where a and h have been already defined.

The general idea is to use an auxiliary function f', where

                       f'(x) = <x,f(x)>

So, f'(0) = < 0, a>, and given the pair p = < x,f(x) > = f'(x), we build the next pair < x+1, f(x+1) > by computing the successor on the first component and applying h to the pair of arguments (that, taking advantage of our encoding of pairs, simply amounts to pass the continuation h as input to the pair p).

Summing up,

next = λp.< succ (fst p), p h>

Finally, to compute f(n) we need to iterate n times the function next starting from < 0, a>, and then take the second component:

 f = λn. snd (n next <0,a>)

这篇关于非递归lambda calculus析因函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！