The Language此次重寫
Closed this issue · 79 comments
與github.com/the-language/js正在重寫。希望能在下個學期開始前完成
文檔未開始寫。
產生了幾種新的語言,它們的單詞將會可以顯示爲各種自然語言的。
新發明特性,設計列表
- 停機問題的避免
- 幾種新的語言
- macro是值
- 優化可用爲平臺定製,並且不混在實現裏。
- 取消數字,完全用優化和庫。
- 無政府的包管理器
- 改進的Effect,Monad系統
- 函數是一種普通的可以分割的東西
- 來源與miniKanren的Sized Lazy,保留計算一個東西的代價
- 有一個內置函數,一般返回第一個,可用因爲優化返回其他的
- miniKanren減少沒有值的情況
- 文本的表示中允許沒有計算完的東西
停機問題的避免
请先在#106 说明怎样算"避免". 之后再讨论其他的.
@nobodxbodon 通過允許編譯解釋器分步的替換沒有值的表達式。
一般的,沒有值是在n次替換後，如果不繼續替換，永遠得不到結果。
實現這個替換可以留到很久以後，因爲比較不重要，難度有點大。
@nobodxbodon 在a=b,b=a等情況時，替換可以產生幾種不同的結果，所以對語言的定義有一些影響。
@nobodxbodon 說明完畢
如果停機問題"被解決"，那麼根據模糊的定義，下面定義的(x)會被替換。所以和停機問題不同。
(define (x)
(if (run-forever? x) '() (x)))我已經說了
實現這個替換可以留到很久以後，因爲比較不重要，難度有點大。
一般的,沒有值是在n次替換後，如果不繼續替換，永遠得不到結果。
@nobodxbodon
替換爲錯誤。
n是任意自然數
@nobodxbodon
替換爲錯誤。
n是任意自然數
@nobodxbodon
替換爲錯誤。
n是任意自然數
@nobodxbodon
替換爲錯誤。
n是任意自然數
@zaoqi-unsafe 先从简单例子开始吧. 如何判断下面是死循环?
while(true) {
;
}
@nobodxbodon 核心語言是lazy函數式的。
是打算把这个特性暂时跳过
實現此特性的方法足夠寫一個什麼樣的Paper,然後發表在什麼什麼地方
這種例子通過直接比較代碼可解決
@zaoqi-unsafe 可否将列表中其他不打算在寒假期间完成的先删去? 再对剩下的每项加些说明(或举个例子), 以便继续讨论?
停機問題的避免 現在是語言文檔中的文字，不需刪去。
文本的表示中允許沒有計算完的東西
是這種東西：（偽Scheme代碼）
(不是被eval的東西 $(() (+ 1 1)))
等於
(不是被eval的東西 2)
核心語言是lazy無副作用的。某些情況下需要這個特性。
macro是值：
macro是一種非基本數據類型。
偽代碼(new-data 'macro '(f))。f是一個函數，類型為Env, ... -> Any。返回的為已經計算好的，不會再eval。
用一種與使用函數不同的語法使用macro。
優化可用爲平臺定製,並且不混在實現裏
編譯解釋器可以優化特定的代碼，因為自然數等東西不是內建的。也允許其他人寫的優化。在代碼更新時，優化自動失效，不會因此產生bug。
無政府的包管理器
這是一個包，可以選擇的一個方案，非內建。
依賴以某種結構直接嵌入代碼里。
編輯器可以自動隱藏依賴的代碼。會實現一個工具自動更新依賴的代碼。
需要無政府的包管理器的一個原因是在某些情況下(航天等)，通訊需要很多時間
函數是一種普通的可以分割的東西
這是已經存在於動態作用域語言的設計
比如某些lisp的(lambda ...)是'(lambda ...)
核心語言沒有動態靜態作用域。沒有提供方便的實現動態作用域的特性，靜態作用域被包實現。
@nobodxbodon 部分没有值的情况已经可以被检测到
@zaoqi 尚未找到相关论文, 但有不少讨论, 如这里的思路:
For example you could write an algorithm that returns "Yes, it terminates" for any program which contains neither loops nor recursion and "No, it does not terminate" for any program that contains a while(true) loop that will definitely be reached and doesn't contain a break statement, and "Dunno" for everything else.
请问你的功能有哪些不同?
这样设计不影响正常算法的书写，也可能可以使解释器能做到总是停机
部分情况是在化简表达式过程中发现循环
在force_all函数里
如果确定要将"可以判断某些无法停止的程序"作为一个特性, 请先说明可判定的程序&输入值范围, 最好有实例(伪代码亦可).
quora链接的例子如下:
Consider the following simple string-rewriting algorithm:
rules = { 'a':'bc', 'b':'a', 'c':'aaa' }
n = int(input())
S = 'a'*n # a string of n 'a's
while len(S) > 1: S = S[2:] + rules[S[0]]
It doesn't get much simpler than this: in each step, remove two letters from the beginning, and append a few new letters at the end. Here's what the program does for n=10 if we print S after each iteration of the while-cycle:
aaaaaaaabc
aaaaaabcbc
aaaabcbcbc
aabcbcbcbc
bcbcbcbcbc
bcbcbcbca
bcbcbcaa
bcbcaaa
bcaaaa
aaaaa
aaabc
abcbc
cbcbc
cbcaaa
caaaaaa
aaaaaaaa
aaaaaabc
aaaabcbc
aabcbcbc
bcbcbcbc
bcbcbca
bcbcaa
bcaaa
aaaa
aabc
bcbc
bca
aa
bc
a
@nobodxbodon 是"没有值",核心是函数式。
替换为错误会影响语言的定义，所以需要写出来。
我的那个解释器现在可以检测
^(#(化滅 (甲) (甲 甲)) (#(化滅 (甲) (甲 甲))))这种
^(#(化滅 (甲) (甲 甲)) (#(化滅 (甲) (甲 甲))))这种
可否用等价的scheme代码演示? 否则新用户估计很难理解.
替换为错误会影响语言的定义，所以需要写出来。
不理解. "替换为错误"是编译器对代码进行的转换? 对程序输出有何影响? 又为何会"影响语言的定义"?
(define (f x) (x x)) (f f)
@nobodxbodon
没有值和那种错误 本来是不等价的
(define (f x) (x x)) (f f)
仅看此例猜不出范围. 是"所有不能收敛的递归"? 自身递归还是可以多函数互相调用的递归? 参数必须是函数本身还是可以是任意值?
如楼上所言, "请先说明可判定的程序&输入值范围"
(define (f x) (x x)) (f f)
仅看此例猜不出范围. 是"所有不能收敛的递归"? 自身递归还是可以多函数互相调用的递归? 参数必须是函数本身还是可以是任意值?
如楼上所言, "请先说明可判定的程序&输入值范围"
@nobodxbodon
語言本身的標準沒有限制。
現在的實現可判斷化簡過程中出現的循環
@nobodxbodon
沒有給語言使用者判定，是替換（解釋）沒有值的表達式為錯誤
這里的值是The Little Typer中的value
你真是愚昧无知到了不可理喻的地步，不仅在我斥责后还来*扰我，而且竟然还*扰Dan Friedman。
听着：
- 你一直在强调「语言允许」但是从来都不对做法进行仔细解释。请问，一个「允许」跟什么都没有有什么差别？
- 假如你做出来了，你的语言就一定不会是图灵完全的，因为你的语言无法表达不停机的程序。假如你竟敢说你的语言“允许”程序员选择是否替换，也只不过是允许程序员将语言变得图灵不完全而已，这样的语言的停机问题当然谁都知道可以解决了，你强调这一点又有什么意义？
- 你口口声声说将「没有值」的部分替换成错误，但是「不停机」就一定「没有值」，所以你一定会需要解决不停机的情况，因此你是在用能解决一个更为困难的问题的方法解决一个不那么困难的问题，而这两个问题在图灵完全的情况下都是绝对不可能解决的。
你的issue不会被reopen也不应该被reopen。你应该就此彻底闭嘴，认真读书，反省你的愚昧言行，将现在的错误想法彻底抛弃。
@bctnry
我可能確實沒有說清楚
替換是由編譯解釋器實現的，使用者不能直接選擇。
我只要可計算的東西能和之前一樣寫出來，並且還可以計算，不需要你說的“Turing完全”。
你口口声声说将「没有值」的部分替换成错误，但是「不停机」就一定「没有值」，所以你一定会需要解决不停机的情况，因此你是在用能解决一个更为困难的问题的方法解决一个不那么困难的问题，而这两个问题在图灵完全的情况下都是绝对不可能解决的。
（define last-try (lambda (x) (and (will-stop? last-try) (eternity x))))這裡 (will-stop? last-try) 和 (last-try '()) 都是沒有值的東西，導致我暫時找不到證明完整的算法不存在的方法
@xieyuheng
好多人沒讀懂，好像有點奇怪：
@bctnry 和Chariette XuQQ:3150038535和@nobodxbodon等人
@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 '())都沒有值(都是不可判定的東西)，所以我暫時想不到證明完整替換算法不存在的方法- 可以計算的有值的還是可以計算的有一樣的值的
@zaoqi
下班的路上再次思考了一下，我觉得你的意思应该是：你的语言集合允许实现者们将能够通过不同的算法分辨出来的不停机的部分替换成错误，但是由于算法本身的不同，所以语义本身也会不同，所以语言本身也会不同，因此你说的不是「语言」而是「语言集合」。
我来告诉你为什么我会这么生气：
- 你在同时说「图灵完全」和「完美判断」，这造成了强烈的「即图灵完全又完美判断的语言」的错觉。这两者当然是不可能同时做到的。
- 「编译器自行判断某些表达式是否不停机」是停机问题，而「编译器自行判断是否做这个替换」依然是停机问题，因此这种定义根本无法“避免”任何问题。
* 你在同时说「图灵完全」和「完美判断」，这造成了强烈的「即图灵完全又完美判断的语言」的错觉。这两者当然是不可能同时做到的。 * 「编译器自行判断某些表达式是否不停机」是停机问题，而「编译器自行判断是否做这个替换」依然是停机问题，因此这种定义根本无法“避免”任何问题。
- 图灵完全
->可计算的算法，正常的算法 可以像Haskell等比较正常的语言一样表达，并且还能正常计算 - 完美判断
->不把有值的表达式当成没有值的表达式 - 停机
->没有值 没有值和不停机有一些区别。因为(define last-try (lambda (x) (and (will-stop? last-try) (eternity x))))的(will-stop? last-try)和(last-try '())都沒有值(都是不可判定的東西)，但(last-try '())是否停机无法判断。
下班的路上再次思考了一下，我觉得你的意思应该是：你的语言集合允许实现者们将能够通过不同的算法分辨出来的不停机的部分替换成错误，但是由于算法本身的不同，所以语义本身也会不同，所以语言本身也会不同，因此你说的不是「语言」而是「语言集合」。
- 没有值与错误本来是不同的东西，这样规定会修改语义
- 同一个实现的同一个版本也可以同时采用不同的替换方案
- _同_一个实现的_同_一个版本也可以_同时_采用_不同_的替换方案
但是依然会产生不同的但是必须要确定为其中一个的语义，最后依然需要依靠某种策略去选择一个，而你以及其他实现者依然需要实现这种策略。
没有值和不停机有一些区别。因为(define last-try (lambda (x) (and (will-stop? last-try) (eternity x))))的(will-stop? last-try)和(last-try '())都沒有值(都是不可判定的東西)，但(last-try '())是否停机无法判断。
然而「不停机」本身也是「没有值」的一种，你依然需要去进行处理，这依然是（或者包含了）停机问题。
(will-stop? last-try)和(last-try '())【是否停机】 无法判断，但【没有值】，所以不能 【用停机问题的方法来】 证明 【不能解决】- 这是一个和停机问题类似但 不同 也没有包含关系 的问题
@bctnry 证明停机问题不能解决是先假设有一个判断是否停机的函数
但
*【没有值】和【不停机】有一些区别
- 代码无法区别替换产生的那种错误和直接构造的那种错误
所以语言本身没法得到一个判断这个语言本身一个表达式有没有值的函数，更没有判断是否停机的
所以用停机问题的方法无法证明这个问题不能解决
- 都沒有值(都是不可判定的東西)
这里正确的说法不是「没有值」，而是「无法判断有没有值」。「没有值」本身就是「没有给出结果」，即「不停机」，因为假如停机，那么它必定有一个结果（正常的值，或是异常等“不正常”的值）。
所以语言本身没法得到一个判断这个语言本身一个表达式有没有值的函数，更没有判断是否停机的
所以用停机问题的方法无法证明这个问题不能解决
假设在语言A之外的某种语言B存在这么一个函数，那么我将语言B转换为语言A就可以得到在语言A里的函数，但是这样的语言A的函数的存在已经被你否定掉了，所以即使在语言之外也不存在这样的函数。
(will-stop? last-try)和(last-try '())都不能是任何值，所以我规定它们为没有值。- 那个是解释语言A的语言B的代码所做的事。在语言A和B中都不能实现那个判断函数。
- 判断不是替换
完整的算法估计很难找到或不存在，因为它可以被用来解决某些未解决数学问题
完整的算法是不存在的，因为这就是停机问题。
- 判断不是替换
判断是替换前必须要做的。确定哪些应该被替换本身就是判断。
- 那个是解释语言A的语言B的代码所做的事。在语言A和B中都不能实现那个判断函数。
- 假设语言B与语言A拥有相同的能力。
- 假设语言B可以实现语言A。
- 由于语言B与语言A拥有相同的能力，那么能用语言B表达的一定也能用语言A表达。
- 假设存在使用语言B的语言A的实现，且该实现中包含该算法。
- 由于3，语言A也应该可以实现该算法。矛盾。
- A確實可以實現一個A的解釋器
- 假設有一個判斷這個語言本身一個表達式有沒有值的算法。
(if 這個表達式沒有值 有值 沒有值)不能是任何值，所以也可以被替換，但是如果有一個判斷算法沒有替換，那麼會出現矛盾，這是 替換 和 判斷 的一個區別
- 假設有一個判斷這個語言本身一個表達式有沒有值的算法。
(if 這個表達式沒有值 有值 沒有值)不能是任何值，所以也可以被替換
你仍然需要判断有哪些表达式跟(if 這個表達式沒有值 有值 沒有值)有一样的效果，因为有同样效果的表达式不止一种，这依然是停机问题。
判断两个表达式是否有相同的效果也是停机问题：假如存在完全正确的算法，用它将别的表达式与不停机的表达式比对就能够得到解决停机问题的算法。
- 好像暫時沒找到是否不停機和是否沒有值不一樣的存在的表達式，但是通過不能成立的假設可以發現有一些區別
判断两个表达式是否有相同的效果也是停机问题：假如存在完全正确的算法，用它将别的表达式与不停机的表达式比对就能够得到解决停机问题的算法。
實現裏沒有/不一定有判断两个表达式是否有相同的效果的東西
- 好像暫時沒找到是否不停機和是否沒有值不一樣的存在的表達式，但是通過不能成立的假設可以發現有一些區別
你变更了「没有值」的定义，所以你的话在你看来会是合理的。
實現裏沒有/不一定有
判断两个表达式是否有相同的效果的東西
这种东西是不存在的，因为它是停机问题的解答，所以它不存在。
- 這種情況是被允許的
那我没有什么好说的了。
@bctnry
之前連值都沒有準確的定義過
我嘗準確精確的試定義一下。
值是頂層有cons,new-XXX,() 這樣的直接構建一個數據結構等表達式
沒有值的表達式 是 在零次或更多次替換後，如果不繼續替換，不能化簡爲任何值的表達式
@nobodxbodon
此處替换指替換沒有值的表達式為某些特定的表達式。
@nobodxbodon
同時我沒有要求全部都要替換掉
@nobodxbodon
一個表達式是否有值 有時和 已經替換了哪些原來沒有值的表達式 有關。