证明 Haskell 语义中的传递性答案

【问题标题】：Prove Transitivity in Haskell semantics [closed]证明 Haskell 语义中的传递性
【发布时间】：2016-12-20 18:36:29
【问题描述】：

我正在学习 Haskell 的语义，在那里我遇到了这个问题：

我已经尝试过了，但仍然无法得出答案。如果有人向我解释如何证明这一点，那就太好了。谢谢。

【问题讨论】：

我投票结束这个问题，因为它不是一个编程问题。
@Renzo 你能告诉我在哪里问这种问题吗？谢谢
你可以试试cs.stackexchange.com或者math.stackexchange.com
这类问题更适合ComputerScience StackExchange。在任何情况下：如果给定s <= s' 和s' <= s''，则应该从定义<= 开始，它拥有s <= s''。然后你使用<= 的定义并检查哪些情况是可能的。 s <= s' 可能成立，因为 s == s'，或者因为有一个 n 这样...... s' <= s'' 相同，您只需逐案证明。
@Bakuriu .. 我也在那里发布了问题，再次感谢您帮助我。我现在试着解决它，你能解释一下第二个问题吗？如何找到这个系列的链。

【解决方案1】：

【讨论】：

你能解释一下，你是如何找到链的。
pn([x,0,0 .. ]) == x 对于任何 n。如果链 x-es 满足传递性，则集合链也 X-es。
谢谢你，但我没明白，pn(x,0,0,0..) 怎么样？，你如何得出这个。你能解释一下吗，因为我还在为这个问题苦苦挣扎。
这可以是链条吗：[0,0,1,1,2,2...]？
陈是元素的陈。一个元素是整数序列，因此要构建链，就需要整数序列链。这个chan必须有序（传递性规则）。两个元素（两个整数序列）的比较定义为通过函数 pn 映射以从整数序列中获取整数，然后进行比较。所以 [0,0,1,1,2,2, ..] 只是单个元素，你需要的是这样的元素链。