问题标签 [ats]

不久前，“ATS”编程语言已从计算机语言基准游戏中删除。您仍然可以通过回程机器查看旧页面。

为什么 ATS 编程语言不再包含在计算机语言基准测试游戏中？

我在 ATS 中编码，并试图创建一个函数来找到给定整数的平方根。这里提供的是正确满足我要求的代码，而不是尾递归。

我不确定其他人是否熟悉这种语言，但这是我使用它的第一周。我知道常规递归和尾递归之间的明显区别，我只是不明白如何改变它。

我什至不需要确切的代码来做到这一点，我只是想知道这怎么可能。为了让我找到 sqrt，我必须计算 n4 = 1 / n，然后将其乘以 2。但是，这样做会进入递归。我想要做的是计算一个结果，然后将它传递给我的下一个递归调用。

这是否意味着我需要以某种方式向后工作？希望这一切都有意义，但如果需要，我会尝试澄清。

谢谢！

funset_nil文件中的声明libats/ML/SATS/funset.sats如下：

是什么:<>意思？

我正在尝试使用该funset_avltree库，但编译器生成了无效的 C 代码。我正在使用 ATS/Postiats 版本 0.2.10。

我的代码相当简单：

然而，编译器的输出相当混乱：

我得到类似的错误funset和funset_listord。我一定错过了一些微不足道的东西。我需要包含一些东西或将一些标志传递给编译器吗？

有人可以告诉我如何在 ATS 中实现以下功能：

谢谢！

在 ATS 代码中，我经常看到两种列表类型：list 和 list0。它们之间有什么区别？

我经常在 ATS 中看到类似以下行的代码：

函数 g0ofg1 看起来像是某种类型的转换。它实际上是做什么的？

例如，我如何在 ATS 中编写与以下 C 代码相对应的内容：

据我了解，以下代码行有效地将 r12 = r0 添加到 Z3 将在类型检查期间尝试满足约束的“环境”中：

prval () = is_fun(pf12, pf0)

认为这实际上是在减少约束的数量是不正确的，因为应用 r12 = r0 可能允许求解器证明两个先前唯一的约束现在是等价的？而且，一旦我们充分减少了约束的数量，归纳假设以及我们的基本案例将提供解决方案的其余部分吗？

我试图大致了解幕后发生的事情，以帮助理解如何在函数式编程中构建证明。

例如，如何构造一个包含所有数字的列表：0、1、2、3、4、5、6、7、8 和 9。