多態(tài)性λ-演算的直觀建模

摘要： 命名綁定是在形式系統(tǒng)中的核心概念之一。至于簡(jiǎn)單性和直觀性，現(xiàn)有的命名綁定技術(shù)有其優(yōu)缺點(diǎn)。通過建模語(yǔ)言HyperLMNtal將一種基于超圖重寫的命名綁定技術(shù)應(yīng)用于具有子類型和結(jié)構(gòu)類型的多態(tài)性λ-演算(或System F_(<:))的類型檢查和按值調(diào)用的建模，并使用PoplMark挑戰(zhàn)的基準(zhǔn)測(cè)試進(jìn)行測(cè)試。實(shí)驗(yàn)結(jié)果表明該技術(shù)適合于復(fù)雜形式系統(tǒng)的快速建模，因?yàn)樗钩绦騿T無(wú)需理論的重新形... （共8頁(yè)）