日々の流転

λ. Pattern matching with dependent types.

T. Coquand. Pattern matching with dependent types. In Proceedings of the International Workshop on Types for Proofs and Programs, 1992.

• <URL:http://www.lfcs.informatics.ed.ac.uk/research/types-bra/proc/>

依存型(dependent type)が存在する場合のパターンマッチングの話。パターンをコンテキストマッピングをして形式化し、パターンマッチによる定義が正しい定義であるための十分条件とチェックのためのアルゴリズムを示している。パターンをコンテキストマッピングとして扱うのが面白かった。例えば以下のような定義の場合、

add : (x : N, y : N)N
add(succ(m),n) = succ(add(m,n))
add(zero, n)   = n

Δ = { x : N, y : N } として、 最初のパターンは { x := succ(m), y := n }: { m : N, n : N } -> Δ 、 二つ目のパターンは { x := zero, y := n }: { n : N } -> Δ というコンテキストマッピングとして扱う。

20050915#p01 に少し追記。