标签: lambda-calculus

我对lambda演算中的前身函数的维基百科描述感到困惑.

维基百科所说的如下:

PRED:=λnfx.n(λgh.h(gf))(λu.x)(λu.u)

有人可以一步一步地解释减少过程吗？

谢谢.

我正在玩Haskell中的一些lambda演算,特别是教堂数字.我有以下定义:

let zero = (\f z -> z)
let one = (\f z -> f z)
let two = (\f z -> f (f z))
let iszero = (\n -> n (\x -> (\x y -> y)) (\x y -> x))
let mult = (\m n -> (\s z -> m (\x -> n s x) z))

这有效:

:t (\n -> (iszero n) one (mult one one))

发生检查时失败:

:t (\n -> (iszero n) one (mult n one))

我iszero和 …

所有,

下面是我发现很难减少的lambda表达式,即我无法理解如何解决这个问题.

(λmλnλaλb.m(nab)b)(λfx.x)(λfx.fx)

这是我试过的,但我被卡住了:

将上述表达式考虑为:(λm.E)M等于
E = (λnλaλb.m (nab)b)
M =(λfx.x )(λfx.fx)

=>(λnλaλb.(λfx.x)(λfx.fx)(nab)b)

考虑到上述表达式为(λn.E)M等于
E =(λaλb.(λfx.x)(λfx.fx)(nab)b)
M = ??

..而我迷路了!!

任何人都可以帮助我理解,对于任何lambda演算表达式,执行还原的步骤应该是什么？

给定一个至少有n参数的函数,我想旋转第一个参数,使它成为n第一个参数.例如(在无类型的lambda演算中):

r(?a. a)                   = ?a. a
r(?a. ?b. a b)             = ?b. ?a. a b
r(?a. ?b. ?c. a b c)       = ?b. ?c. ?a. a b c
r(?a. ?b. ?c. ?d. a b c d) = ?b. ?c. ?d. ?a. a b c d

等等.

你能用r通用的方式写吗？如果你知道n >= 2怎么办？

这是Scala中陈述的问题:

trait E
case class Lam(i: E => E) extends E
case class Lit(i: Int) extends E
case class Ap(e: E, e: E) …

我已经看到了教会Rosser定理的多个参考,特别是钻石属性图,同时学习函数式编程,但我没有遇到过一个很好的代码示例.

如果像Haskell这样的语言可以被视为一种lambda演算,那么必须能够使用语言本身来演示一些例子.

如果示例轻松地显示步骤或减少如何导致易于并行执行,我会给予奖励积分.

Haskell 定义说:

表达式是弱头正常形式(WHNF),如果它是:

• 一个构造函数(最终应用于参数),如True,Just(square 42)或(:) 1
• 一个内置函数应用于太少的参数(可能没有),如(+)2或sqrt.
• 或lambda抽象\ x - >表达式.

为什么内置功能会得到特殊处理？根据lambda演算,部分应用函数和任何其他函数之间没有区别,因为最后我们只有一个参数函数.

我正在为交互网编译lambda演算术语,以便使用Lamping的抽象算法来评估它们.为了测试我的实现,我使用了这个教堂号码除法功能:

div = (? a b c d . (b (? e . (e d)) (a (b (? e f g . (e (? h . (f h g)))) (? e . e) (? e f . (f (c e)))) (b (? e f . e) (? e . e) (? e . e)))))

除以4(即(? k . (div k k)) (? f x . (f (f (f (f x)))))),我得到这个网:

(抱歉可怕的渲染.?是一个lambda,R是root,D是粉丝,e是橡皮擦.) …

我正在通过类型和编程语言,而Pierce,通过降价策略调用,给出了该术语的示例id (id (?z. id z)).在将外部折射率降低到正常形式之前,将内部折射率id (?z. id z)减小到?z. id z第一次,id (?z. id z)作为第一次减少的结果?z. id z.

但是,按价值顺序调用被定义为"只有最外层的重新索引被减少",并且"仅当其右侧已经减少到某个值时,才会减少重新索引".在示例中id (?z. id z)出现在最外层redex的右侧,并且减少了.这与只有最外层的指数减少的规则相比如何？

"最外层"和"最内层"的答案仅仅是指lambda抽象吗？因此,对于一个长期t的?z. t,t不能减少,但在归约s t,t减少到一个值v,如果这是可能的,然后s v被降低？

class Monad m where
  return :: a -> m a
  (>>=)  :: m a -> (a -> m b) -> m b
  (>>)   :: m a -> m b -> m b
  m >> n = m >>= \_ -> n

  fail   :: String -> m a

我以前从未在类型类中看过方程式(或函数声明？).为什么在类型类中有一个等式？

我知道_是一个匹配任何东西的术语.但是m >> =\_ - > n匹配？

在OCaml中,拥有以下内容是合法的.mli:

val f : 'a -> 'a
val g : 'a -> 'a

并且.ml:

let f x = x
let g = f

然而在F#中,这被拒绝了:

eta_expand.ml(2,5): error FS0034: Module 'Eta_expand' contains
    val g : ('a -> 'a)    
but its signature specifies
    val g : 'a -> 'a    

The arities in the signature and implementation differ. The signature specifies that 'g' is function definition or lambda expression accepting at least 1 argument(s), but the implementation is a computed …