小编Raf*_*tro的帖子

在Haskell中有一个术语undefined :: a,据说是一个坏计算或无限循环的术语表示.由于undefined具有类型a,因此可以通过应用类型替换来创建任何语法正确类型.所以undefined有任何类型,o反过来也是如此:任何类型都有undefined,这是生活在任何类型内部的底值(包括Void类型,对吧？).

库里 - 霍华德同构提供的不仅仅是命题作为类型,它还给出了习惯类型作为定理.

具有所有命题作为定理的逻辑系统被认为是不一致的.

那么,Haskell的类型系统是否与不一致的逻辑系统同构？

如果是这样,后果是什么？

如果Haskell的类型系统是一个不一致的证明系统,我们不能相信它吗？

有可能代表无限循环undefined吗？

我需要做一个线性近似。但是，它必须是对数刻度。

这是我的gnuplot脚本：

f(x)= a*x+b
fit f(x) "d0.dat" via a,b
set logscale x
set logscale y
plot "d0.dat" with points lt rgb "#ff0000" title "Points", \
f(x) with lines lt rgb "#ff00ff" title "Approximation"

显然，这种近似是错误的。谁能帮我修复它。我在Google中找不到任何东西。

为了通过一个良好的关系理解递归，我决定实现扩展的欧几里得算法。

扩展的欧几里得算法适用于整数，因此我需要一些关于整数的良好依据。我尝试使用中的关系Zwf，但没有任何效果（我需要查看更多示例）。我认为使用该函数映射Z起来会更容易，然后将其用作关系即可。我们的朋友来帮助我。所以这是我做的：natZ.abs_natNat.ltwf_inverse_image

Require Import ZArith Coq.ZArith.Znumtheory.
Require Import Wellfounded.

Definition fabs := (fun x => Z.abs_nat (Z.abs x)). (* (Z.abs x) is a involutive nice guy to help me in the future *) 
Definition myR (x y : Z) := (fabs x < fabs y)%nat.
Definition lt_wf_on_Z := (wf_inverse_image Z nat lt fabs) lt_wf.

扩展的欧几里得算法如下所示：

Definition euclids_type (a : Z) := forall b : Z, Z * Z * Z.

Definition euclids_rec …

我正在尝试插入两个这样的列表:

intercalate [0, 2, 4] [1, 3, 5]
[0, 1, 2, 3, 4, 5]

所以我创建了这个函数:

intercalate (x:xs) (y:ys) = x:(y:(intercalate xs ys))
intercalate [] [] = []

但是我总是得到这个错误:

 Exception: <interactive>:3:5-57: Non-exhaustive patterns in function intercalate

我不明白为什么!