The Language此次重寫

[zaoqi-unsafe]

與github.com/the-language/js正在重寫。希望能在下個學期開始前完成 文檔未開始寫。 產生了幾種新的語言,它們的單詞將會可以顯示爲各種自然語言的。

[zaoqi]

@nobodxbodon 沒什麼參考資料。

• 這個語言是函數式，懶惰求值的，求值時無副作用，副作用用類似Haskell的Monad,Idris的Effect的格式表示
• 錯誤是一種值，可以在類型判斷（pair?這種）的地方對於錯誤進行特殊處理，參數爲錯誤時(...? <錯誤>)也是一個錯誤
• 語言本身允許編譯器解釋器替換儘量小的沒有值的表達式爲錯誤
• 對於(f0 ...(f ... <一個沒有值> ...) ...)，如果f0 ... f是幾個需要<一個沒有值>化簡爲值才能返回一個表達式的內建函數，則只替換<一個沒有值>爲錯誤，不爲了<一個沒有值>替換整個(f0 ...(f ...) ...)
• 替換可以分步進行，每次可以替換任意個。
• a=(car b),b=(car a)等情況下一個有多種合理的替換方案，導致一個表達式可以有多個合理的替換後的值
• （define last-try (lambda (x) (and (will-stop? last-try) (eternity x))))的(will-stop? last-try)和(last-try '())都沒有值(都是不可判定的東西)，所以我暫時想不到證明完整替換算法不存在的方法
• 可以計算的有值的還是可以計算的有一樣的值的

[bctnry]

@zaoqi 下班的路上再次思考了一下，我觉得你的意思应该是：你的语言集合允许实现者们将能够通过不同的算法分辨出来的不停机的部分替换成错误，但是由于算法本身的不同，所以语义本身也会不同，所以语言本身也会不同，因此你说的不是「语言」而是「语言集合」。

我来告诉你为什么我会这么生气：

• 你在同时说「图灵完全」和「完美判断」，这造成了强烈的「即图灵完全又完美判断的语言」的错觉。这两者当然是不可能同时做到的。
• 「编译器自行判断某些表达式是否不停机」是停机问题，而「编译器自行判断是否做这个替换」依然是停机问题，因此这种定义根本无法“避免”任何问题。

[zaoqi]

@bctnry

* 你在同时说「图灵完全」和「完美判断」，这造成了强烈的「即图灵完全又完美判断的语言」的错觉。这两者当然是不可能同时做到的。

* 「编译器自行判断某些表达式是否不停机」是停机问题，而「编译器自行判断是否做这个替换」依然是停机问题，因此这种定义根本无法“避免”任何问题。

• 图灵完全 -> 可计算的算法，正常的算法 可以像Haskell等比较正常的语言一样表达，并且还能正常计算
• 完美判断 -> 不把有值的表达式当成没有值的表达式
• 停机 -> 没有值
• 没有值和不停机有一些区别。因为(define last-try (lambda (x) (and (will-stop? last-try) (eternity x))))的(will-stop? last-try)和(last-try '())都沒有值(都是不可判定的東西)，但(last-try '())是否停机无法判断。

[zaoqi]

@bctnry

下班的路上再次思考了一下，我觉得你的意思应该是：你的语言集合允许实现者们将能够通过不同的算法分辨出来的不停机的部分替换成错误，但是由于算法本身的不同，所以语义本身也会不同，所以语言本身也会不同，因此你说的不是「语言」而是「语言集合」。

• 没有值与错误本来是不同的东西，这样规定会修改语义
• 同一个实现的同一个版本也可以同时采用不同的替换方案

[bctnry]

@zaoqi

• _同_一个实现的_同_一个版本也可以_同时_采用_不同_的替换方案

但是依然会产生不同的但是必须要确定为其中一个的语义，最后依然需要依靠某种策略去选择一个，而你以及其他实现者依然需要实现这种策略。

• 没有值和不停机有一些区别。因为(define last-try (lambda (x) (and (will-stop? last-try) (eternity x))))的(will-stop? last-try)和(last-try '())都沒有值(都是不可判定的東西)，但(last-try '())是否停机无法判断。

然而「不停机」本身也是「没有值」的一种，你依然需要去进行处理，这依然是（或者包含了）停机问题。

[zaoqi]

@bctnry

• (will-stop? last-try)和(last-try '())【是否停机】 无法判断，但【没有值】，所以不能 【用停机问题的方法来】 证明 【不能解决】
• 这是一个和停机问题类似但 不同 也没有包含关系 的问题

[zaoqi]

@bctnry 证明停机问题不能解决是先假设有一个判断是否停机的函数 但

*【没有值】和【不停机】有一些区别

• 代码无法区别替换产生的那种错误和直接构造的那种错误

所以语言本身没法得到一个判断这个语言本身一个表达式有没有值的函数，更没有判断是否停机的 所以用停机问题的方法无法证明这个问题不能解决

[bctnry]

@zaoqi

• 都沒有值(都是不可判定的東西)

这里正确的说法不是「没有值」，而是「无法判断有没有值」。「没有值」本身就是「没有给出结果」，即「不停机」，因为假如停机，那么它必定有一个结果（正常的值，或是异常等“不正常”的值）。

所以语言本身没法得到一个判断这个语言本身一个表达式有没有值的函数，更没有判断是否停机的 所以用停机问题的方法无法证明这个问题不能解决

假设在语言A之外的某种语言B存在这么一个函数，那么我将语言B转换为语言A就可以得到在语言A里的函数，但是这样的语言A的函数的存在已经被你否定掉了，所以即使在语言之外也不存在这样的函数。

[zaoqi]

@bctnry

• (will-stop? last-try)和(last-try '())都不能是任何值，所以我规定它们为没有值。
• 那个是解释语言A的语言B的代码所做的事。在语言A和B中都不能实现那个判断函数。
• 判断不是替换

[zaoqi]

@bctnry 完整的算法估计很难找到或不存在，因为它可以被用来解决某些未解决数学问题

[bctnry]

@zaoqi

完整的算法估计很难找到或不存在，因为它可以被用来解决某些未解决数学问题

完整的算法是不存在的，因为这就是停机问题。

• 判断不是替换

判断是替换前必须要做的。确定哪些应该被替换本身就是判断。

[bctnry]

@zaoqi

• 那个是解释语言A的语言B的代码所做的事。在语言A和B中都不能实现那个判断函数。

1. 假设语言B与语言A拥有相同的能力。
2. 假设语言B可以实现语言A。
3. 由于语言B与语言A拥有相同的能力，那么能用语言B表达的一定也能用语言A表达。
4. 假设存在使用语言B的语言A的实现，且该实现中包含该算法。
5. 由于3，语言A也应该可以实现该算法。矛盾。

[zaoqi]

@bctnry

• A確實可以實現一個A的解釋器
• 假設有一個判斷這個語言本身一個表達式有沒有值的算法。(if 這個表達式沒有值 有值 沒有值)不能是任何值，所以也可以被替換，但是如果有一個判斷算法沒有替換，那麼會出現矛盾，這是 替換 和 判斷 的一個區別

[bctnry]

@zaoqi

• 假設有一個判斷這個語言本身一個表達式有沒有值的算法。(if 這個表達式沒有值 有值 沒有值)不能是任何值，所以也可以被替換

你仍然需要判断有哪些表达式跟(if 這個表達式沒有值 有值 沒有值)有一样的效果，因为有同样效果的表达式不止一种，这依然是停机问题。

[zaoqi]

@bctnry 爲何需要找到一樣效果的表達式

[zaoqi]

@bctnry

該算法可能是判斷被解釋的語言的經過0次或更多次替換後的表達式的全部或一部分是否沒有值。

[zaoqi]

@bctnry

这依然是停机问题。

我好像無法看懂這句話

[bctnry]

@zaoqi

爲何需要找到一樣效果的表達式

不找到就会出现“没有值”但是“没有转变成错误”的情况。

[bctnry]

@zaoqi

我好像無法看懂這句話

判断两个表达式是否有相同的效果也是停机问题：假如存在完全正确的算法，用它将别的表达式与不停机的表达式比对就能够得到解决停机问题的算法。

[zaoqi]

@bctnry

不找到就会出现“没有值”但是“没有转变成错误”的情况。

• 這種情況是被允許的
• 那個東西的假設不能成立，所以它實際上不存在

[zaoqi]

@bctnry

判断两个表达式是否有相同的效果也是停机问题：假如存在完全正确的算法，用它将别的表达式与不停机的表达式比对就能够得到解决停机问题的算法。

• 好像暫時沒找到是否不停機和是否沒有值不一樣的存在的表達式，但是通過不能成立的假設可以發現有一些區別

[zaoqi]

@bctnry

判断两个表达式是否有相同的效果也是停机问题：假如存在完全正确的算法，用它将别的表达式与不停机的表达式比对就能够得到解决停机问题的算法。

實現裏沒有/不一定有判断两个表达式是否有相同的效果的東西

[bctnry]

@zaoqi

• 好像暫時沒找到是否不停機和是否沒有值不一樣的存在的表達式，但是通過不能成立的假設可以發現有一些區別

你变更了「没有值」的定义，所以你的话在你看来会是合理的。

實現裏沒有/不一定有判断两个表达式是否有相同的效果的東西

这种东西是不存在的，因为它是停机问题的解答，所以它不存在。

• 這種情況是被允許的

那我没有什么好说的了。

[zaoqi]

@bctnry

那我没有什么好说的了。

我沒有要求全部都替換，是允許替換一部分或全部或不替換。

[zaoqi]

@bctnry 之前連值都沒有準確的定義過 我嘗準確精確的試定義一下。 值是頂層有cons,new-XXX,() 這樣的直接構建一個數據結構等表達式 沒有值的表達式 是 在零次或更多次替換後，如果不繼續替換，不能化簡爲任何值的表達式

[nobodxbodon]

@zaoqi

沒有值的表達式 是 在零次或更多次替換後，如果不繼續替換，不能化簡爲任何值的表達式

之前忘了回, 又回到之前的问题: "替换几次"?

先退一步说, 你的语言中, 一个表达式, 最多需要替换几次之后简化为值? 如果可以是任意次, 那么就无法仅依靠替换次数的阈值来严格判断这个表达式是否"没有值".

[zaoqi]

@nobodxbodon 此處替换指替換沒有值的表達式為某些特定的表達式。

[zaoqi]

@nobodxbodon 同時我沒有要求全部都要替換掉

[zaoqi]

@nobodxbodon 一個表達式是否有值 有時和 已經替換了哪些原來沒有值的表達式 有關。