2009/01/31

Algebra of programming in Agda: dependent types for relational program derivation

中文摘要:

關係式程式推導(relational program derivation)是「以代數規則將關係式規格(relational specification)逐步特化為程式」的技巧。因為建構過程的保證,如此得到的程式必然是正確的。另一方面,依值型別理論(dependent type theory)已發展得十分豐富,足以表達多種正確性質且可透過型別檢驗加以驗證。

我們造了一套程式庫 AoPA,使用者可在支援依值型別的程式語言 Agda 中編寫關係式推導。每個程式都附帶一個代數推導,由型別系統擔保其正確性。

我們提出兩個有意思的例子:一個最佳化問題和快速排序的推導,後者用良基遞迴(well-founded recursion)在支援歸納式型別(inductive types)的語言中模映「計算終必停止的生滅式」(terminating hylomorphisms)。

嘔,好噁心的翻譯(特別是把所有名詞都譯出來之後 ─「生滅式」還滿惡搞的 XD)。要看原文摘要和 paper 請到 scm 老師的官方網頁

--
是太久沒翻譯還是這段本來就難譯啊?不知道這個問題的答案代表可能是前者 XD。

Labels: , ,

Blogger yen31/31/2009 5:33 pm 說:

我會盡力看懂,不過英文真的比較好懂,或許是因為英文看習慣的關係吧XD

 
Anonymous Anonymous2/02/2009 5:37 am 說:

啊,「良基遞迴」呢! XD

 

<< 回到主頁