概念

我正在实现一个解释器，它允许用户定义任意组合器并将它们应用于任意术语。例如，用户可以通过输入以下组合子定义来定义对的Church 编码：

然后用户可以输入first (pair a b)，根据之前定义的规则逐步减少：

也可以定义其他组合子，例如在SKI 组合子演算中使用的那些：

身份组合器也可以根据前两个组合器由I → S S K KorI → S K (K K)或来定义I = S K x。然后可以通过以下方式定义通用iota 组合器：

这些例子希望能说明我正在尝试做的事情。

执行

我正在尝试使用图形缩减和图形重写系统来实现这一点。让tree是递归定义的数据类型

这是一棵二叉树，其中节点可以是叶子（终端节点）或由一对子树组成的分支（内部节点）。分支代表一个术语对另一个术语的应用，而叶子代表组合子和参数。让我们rule定义一个数据类型

这对应于将左树转换为右树 (a → b) 的归约规则。的列表rules然后可以定义为

有效地，当评估一个表达式时pair a b c → c a b，解释器构造一棵(((pair a) b) c)对应于左侧形式的树，一棵对应于右手边形式的树((c a) b)，构造一对对应于 a 的两棵树rule（其中a,b,c以某种方式指定是任意参数，不一定是组合符或终结符号），并将这对附加到列表中rules。当减少形式的表达时first (pair a b)，解释器构造相应的树(first ((pair a) b))并应用归约规则，如下所示：

为此，解释器必须对树及其子树执行模式匹配，“移动”组合子和任意参数以构造对应于规则右侧的新树。C中树结构的示例实现由下式给出

模式匹配函数可以实现为

但是，我不确定如何实施此过程的重要细节，包括：

1. 将输入树与归约规则的 LHS 树匹配。
2. 将输入树转换为归约规则的 RHS 树，保留参数（可能是树叶或树枝）并将它们“移动”到适当的位置。

我相信节点上的模式匹配将涉及检查节点的左孩子和右孩子等等，直到到达终端节点。有谁知道在 C 中实现了类似概念并且我可以从中学习的在线程序或教程？通过这种方法解决问题，我是否走在正确的轨道上，还是有更简单的方法？

我正在使用 Coq 完成一些介绍级别的组合逻辑练习。我已经为它编写了一个粗略的库，但它不是很有效。是否有用于 Coq 或其他证明助手的组合逻辑库？组合子、术语及其关系的定义以及一些重要定理的证明将非常有帮助。

有一个关于 Agda 和组合逻辑的讨论看起来很有趣，但我不知道它是否与我的问题相关。

我正在尝试使用 lambda 演算功能实现概率 ccg。

基本上我想做以下代码：

但是现有的 NLTK 的 CCG 实现不支持词典中的 {sem=\x.he(x)} [1.0] 种语义部分。

是否有任何其他 CCG 实现可以处理这个问题？或者我可以在 NLTK 中代表这个吗？

我想在 Haskell 中快速正确地减少函数以指向自由形式。我更愿意产生相当可读的结果。我该怎么办？

我对滑雪组合器有疑问。

XOR（异或）只能使用S 和K组合子来表达吗？

我有

在哪里

有没有办法在 Ceylon 中实现某种递归类型的函数？例如，我可以在 Ceylon 中以类型安全的方式定义组合逻辑，如下所示：

此代码按预期工作。但是，为了清晰、简洁和适用于其他问题，我希望能够仅使用函数来实现此行为。采取类似以下（非工作）示例：

在函数别名版本中，Fi 类型表示其操作数和返回值可以无限组合的函数。请注意，由于它们的递归性质，类型 Fi、Fi(Fi) 和 Fi(Fi)(Fi) 可以被认为在功能上是等效的；他们中的任何一个的消费者所知道的是，如果他们有一个函数，如果在一个 Fi 上调用，就会给他们另一个 Fi。

以下是我对 Ceylon 目前支持的内容的理解：

• 由于在编译期间被擦除，因此不支持递归别名。
• 我不知道当前有任何 Ceylon 功能可用于递归地专门化 Callable 类型或以其他方式获得所需的无限链接。
• 一个可能相关的问题得到了否定的答复。然而，那是两年半前的事了，在 Ceylon 1.2 和 Gavin King 写的关于新类型函数支持的博客中实现了一些可能相关的特性（如类型函数）之前。
• 高阶泛型有一个github 问题。
• 关于允许 Callable 的自定义实现还有另一个github 问题。

可以在当前版本的 Ceylon 中实现所需的行为吗？或者它肯定需要上述积压功能中的一项或两项？

我正在努力解决问题，但你能在代码战上滑雪吗？它即将在 SKI 组合器中表达 lambda。来源在https://repl.it/@delta4d/SKI。

经过一些研究，尤其是组合逻辑，我能够解决除xor.

我首先将 xor 翻译成

这是

将 lambda 应用于 SKI 规则，我得到了

我检查了http://ski.aditsu.net上的 SKI 演示文稿，效果很好。

Haskell 源代码编译，但出现运行时错误。

代码战报告：

我在本地进行了测试prettyPrintSKI $ Ap (Ap xor' false) true，它报告：

无限类型是什么？什么是刚性类型？

我在oras上做同样的事情or = \x y -> x true y，它工作得很好。

1. https://www.codewars.com/kata/sure-but-can-you-ski-i
2. https://en.wikipedia.org/wiki/Combinatory_logic
3. http://ski.aditsu.net

id( ¹ P ₁ ) 和const( ² P ₁ )等投影函数在函数式编程中非常有用。但是，有时您需要更复杂的投影函数，例如⁵ P ₄。您可以用点式的方式手动编写它，a => b => c => d => e => d但这很乏味且可读性不强。因此，能够改写会更好proj(5)(4)。以下是我目前在 JavaScript 中定义这个广义投影函数的方式：

如您所见，这种实现proj是一种 hack，因为它使用了可变参数。因此，它不能直接翻译成 Agda 或 Idris 之类的语言（由于依赖类型，广义投影函数实际上是可类型化的）。那么，如何递归地定义一个广义投影函数，使其可以直接翻译成 Agda 呢？

我正在关注这篇博文：http ://semantic-domain.blogspot.com/2012/12/total-functional-programming-in-partial.html

它展示了一个用于System T（一种简单的全功能语言）的小型 OCaml 编译器程序。

整个管道采用 OCaml 语法（通过 Camlp4 元编程）将它们转换为 OCaml AST，然后再转换为 SystemT Lambda Calculus（参见module Term：），最后是 SystemT Combinator Calculus（参见：） module Goedel。最后一步也用 OCaml 元编程Ast.expr类型包装。

我试图在不使用 Template Haskell 的情况下将其翻译成 Haskell。

对于 SystemT Combinator 表单，我将其写为

请注意，这Compose是前向合成，不同于(.).

在 SystemT Lambda Calculus 到 SystemT Combinator Calculus 的转换过程中，该Elaborate.synth函数尝试将 SystemT Lambda 演算变量转换为一系列组合投影表达式（与 De Brujin 指数相关）。这是因为组合演算没有变量/变量名称。这是通过Elaborate.lookupwhich 使用Quote.find函数来完成的。

问题是我将组合微积分编码为 GADT THom a b。翻译Quote.find函数：

进入哈斯克尔：

导致无限类型错误。

问题源于这样一个事实，即使用和Compose来自GADT会导致类型签名的无限变化。FstSndTHom a b

该文章没有这个问题，因为它似乎使用Ast.exprOCaml 东西来包装底层表达式。

我不确定如何在 Haskell 中解决。我应该使用存在量化的类型，例如

或者某种类型级别Fix来适应无限类型问题。但是我不确定这如何改变findorlookup功能。

在上一个问题SystemT Compiler and handling Infinite Types in Haskell 中，我询问了如何将 SystemT Lambda Calculus 解析为 SystemT Combinators。我决定使用纯代数数据类型来编码 SystemT Lambda 演算和 SystemT Combinator 演算（基于评论：SystemT Compiler and processing Infinite Types in Haskell）。

SystemTCombinator.hs：

SystemTLambda.hs：

我使用上面的双向类型检查器解析SystemTLambda.TTerm成SystemTCombinator.THom.

组合子表达式为：

我现在遇到的问题是如何解释这个组合子表达式。我知道所有组合子表达式都应该被解释为一个函数。问题是我不知道这个函数的输入和输出类型，我希望“解释器”函数是部分的，因为如果它试图错误地解释某些东西，它应该会导致 aRuntimeException因为组合表达式是无类型，可能有错误的组合表达式。然而，我的类型检查器应该确保一旦到达解释器，组合器就应该已经很好地输入了。

根据原始博客文章，http://semantic-domain.blogspot.com/2012/12/total-functional-programming-in-partial.html组合器具有所有功能等价物。就像是：

但显然这行不通。似乎必须有某种方式来解释THom树，这样我才能得到某种功能，可以以部分方式执行。