问题标签 [church-encoding]

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

0 投票
1 回答
1774 浏览

compiler-errors - Coq 中的“错误:宇宙不一致”是什么意思?

我正在研究软件基础,​​目前正在做关于教堂数字的练习。这是自然数的类型签名:

我定义了一个succ类型的函数nat -> nat。我现在想定义一个加法函数,如下所示:

但是,我收到以下错误消息:

此错误消息实际上是什么意思?

0 投票
3 回答
721 浏览

list - 教会编码列表的更有效的尾部

这是一个有文化的haskell帖子。只需将其保存为“ChurchList.lhs”即可运行。

Church 编码列表是一种通过函数表示列表的方式。它类似于弃牌和连续传球风格。

为了说明这如何对应于一个列表,这里是一个 O(n) 同构

这些东西具有良好的性能特征。

现在,问题来了tail

基本上我的实现所做的是将列表分成头部和尾部。Cons 替换了头部,并将旧的头部附加到尾部。这是相当低效的。似乎教会列表在拆分方面通常效率低下。

我希望我错了。有没有tailCl比 O(n) 更好的实现(最好是 O(1))。

0 投票
1 回答
325 浏览

recursion - 方案中教堂数字的递归

根据维基百科的定义,我在教堂数字上定义了教堂数字零和其他一些标准功能,如下所示:

使用这些,我将递归循环编写为:

现在对于n0上述参数,这应该返回n0,而不进入递归。但事实并非如此。为什么?

注 1:此递归循环与普通数字和普通函数完美配合:

0将按原样返回。

注意 2:函数ifthenelse, iszero, newtrue,newfalse也可以自己正常工作。

0 投票
1 回答
395 浏览

javascript - javascript 中的 Y-Combinator 阶乘适用于数字,而不适用于 Church 数字。

我设法在 javascript 中使用 ES6 箭头函数实现 Church 编码和 Y-Combinator。但是当我试图评估阶乘函数时,

我收到“未捕获 RangeError:超出最大调用堆栈大小(…)”错误。

如果我改变 FactGen,

它只是工作。

我想知道的是它的教堂数字版本。我怎样才能做到这一点?

0 投票
1 回答
338 浏览

swift - 具有不接受输入参数类型的通用参数类型的 Swift 高阶函数(Church pair aka cons)

我在 Swift 2.1 中搞乱了函数式编程,试图实现Church 编码对/cons函数(cons = λx λy λf fxy in untyped lambda calculus),我读过这在早期版本的 Swift 中无法完成。

使用泛型它看起来像

这不起作用,并给出了我无法理解的错误(类型(Int,Int)的参数列表肯定可以匹配泛型类型变量(S,T)?)

如果您摆脱泛型类型,并将它们全部声明为 Ints,则该函数可以工作,但是我们当然希望能够将长度超过 2 的列表组合在一起;例如,使用长度为 3 的列表是使用 (Int,Int) -> Int 来使用 Int。

另一种选择是将所有内容输入为Any(请参阅Type Casting for Any 和 AnyObject),但我也无法做到这一点。

你有什么想法?这在 Swift 中是否可行?我确信有更简单的方法来实现cons/ car/ cdr,但我对 Church 编码特别感兴趣,其中列表元素是匿名函数 (lambdas) 的参数。

0 投票
2 回答
480 浏览

haskell - 在 Haskell 中实现多态 λ-演算/系统 F 对的 Church 编码

我想在 Haskell 的多态 lambda 演算中实现该对的 Church 编码。

在彼得塞林格关于 lambda 演算的笔记的第 77 页第 8.3.3 节中,他给出了两种类型的笛卡尔积的构造:

A×B = ∀α.(A→B→α)→α<br/> ⟨M,N⟩ = Λα.λf A→B→α</sup>.fMN

对于另一个来源,在第 54 页,Dider Rémy 关于 lambda 演算的笔记的第 4.2.3 节,他将多态 λ-演算/系统 F 中对的 Church 编码定义为

Λα₁.Λα₂.λx₁:α₁.λx₂:α₂.Λβ.λy:α₁→α₂→β。y x₁ x₂</p>

我认为雷米和塞林格说的一样,只是更冗长。

无论如何,根据维基百科,Haskell 的类型系统是基于System F的,所以我希望可以直接在 Haskell 中实现这种 Church 编码。我有:

但我不确定如何进行预测。

Λα.Λβ.λp α×β .pα(λx α .λy β .x)

我是否使用 Haskellforall作为大写 lambda 类型量词?

这与我之前的问题基本相同,但使用的是 Haskell 而不是 Swift。我认为额外的背景和场地的变化可能会使它更明智。

0 投票
1 回答
96 浏览

monads - 自由单子是教堂数字吗?

一位评论员最近表示

自由单子是教堂数字——只是使用(endo-)函子而不是函数!

他继续解释这句话:

它们都是由 0 - n 次组成的 endofunct(ion|or)

我知道教堂数字是一组匿名函数组合,每个数字都有一个组合。我只是不明白这如何适用于 Free Monads。

我的问题是:自由单子是教堂数字吗?

0 投票
1 回答
127 浏览

lambda-calculus - 无法推断出 lambda 表达式 λx.λy.x(xy) 的数字表示(教堂编码)

我有一个 lambda 表达式:λx.λy.x(xy),我应该推断它的整数表示。我已经阅读了很多关于教堂编码和教堂数字的具体内容,但我找不到数字是什么。您能否以 3 岁的孩子可以理解的方式向我解释或向我推荐比维基百科更好的资源?

0 投票
1 回答
144 浏览

haskell - 这个haskell表达式是什么意思

我刚开始学习 Haskell,我正在尝试在 Haskell 中使用 lambda 演算。我发现这个表达式将教堂数字转换为数字,但我似乎无法弄清楚这个表达式中的 0 是什么意思。我在任何地方都找不到它:

这是最后一个让我感到困惑的零。它是这个 lambda 表达式的基本情况还是某些参数?

0 投票
1 回答
528 浏览

sml - Lambda 演算 (SML) - 将一个教堂号码应用于另一个

我试图了解 Church 数字的幂函数:

在其中,我看到了一个乘法。我知道这是错误的,因为乘法是:

我想我已经明白了。

问题是我无法理解是什么功能产生了将教堂号码应用于另一个。

例如,这个表达式会产生什么?

谢谢