2009/03/18

Every suc is a free name

盯著這兩條規則看,一陣子後得到結論 ─ 名字的傳遞要分開處理。自從為 Proc type 加上一個 natural number index n 表示有 n 個 free names 之後,情況似乎滿樂觀,已解決規則的 side conditions 都自然地表達在 encoding 裡面。De Bruijn index 和「把 context 編在 type 裡面」的手法湊在一起,就有了一句口號:給我一個 suc,我就送你一個免費的名字 XD。

今日飲食:中午沙茶豬肉麵 @ 男一麵食部($50);晚上鍋燒烏龍麵 @ 老爺上菜($80)+ 巧克力葡萄奶酥麵包 @ 男一麵包店($18)。合計 $148。

--
應該有人觀察出規律了吧?XD

Labels:

Blogger XOO3/19/2009 9:41 am 說:

Conor McBride 有篇 "I am not a number: I am a free variable"
乍聽之下還滿像的 XD

 
Anonymous scm3/21/2009 6:53 am 說:

啊,似乎確實有關:

In this paper, we show how to manipulate syntax with binding using a mixed representation of names for free variables (with respect to the task inhand) and de Bruijn indices for bound variables....

這次又要靠 Conor 了嗎?

 

<< 回到主頁