1.. 하향식 타입 유추 알고리즘 M의 속성 증명
(Proofs About a Folklore Let-Polymorphic Type Inference Algorithm M)
이 욱 세 이 광 근
(Oukseh Lee) (Kwangkeun Yi)
요 약 Hindley Milner 스타일의 복합형 타입 시스템(let-polymorphic type system)을 구현하는 타입 유추 알고리즘은 두 가지가 있다. 하나는 사실상 표준인 상향식(bottom-up) 알고리즘 W이고, 다른 하나는 하향식(top-down) 알고리즘 M이다. W 알고리즘은 안전성(soundness)과 완전성(completeness)이 수학적으로 검증되어 있고 가장 널리 쓰이기는 하지만, 타입 오류가 있는 입력 프로그램에 대해 때때로 모호한 메시지를 만들어 내는 문제점이 있다. 이에 M 알고리즘이 대안이 될 수 있는지를 확인할 필요가 있다. 하지만, 이 알고리즘은 단지 구현상에서 사용되었을 뿐, 정확하게 정의되어 있지 않고, 타입 시스템을 충실히 구현하는지(sound-and-completeness)도 증명되지 않았으며, W 알고리즘과 다른 점도 정확하게 규명되어 있지 않다. 본 논문에서는 M 알고리즘을 정확하게 기술하고, 복합형 타입 시스템을 충실히 구현함을 증명하며, 타입 오류가 있는 입력에 대해 W 알고리즘보다 신속히 타입 오류를 감지하는 성질을 증명한다. 본 논문에서의 증명은 실제 사용되었던 알고리즘에 대한 이론적인 검증인 것이다.
Abstract The Hindley Milner let-polymorphic type inference system has two different algorithms one is the de facto standard W algorithm that is bottom-up or context-insensitive and the other is a folklore algorithm that is top-down or context...
· 해피레포트는 다운로드 받은 파일에 문제가 있을 경우(손상된 파일/설명과 다른자료/중복자료 등) 1주일이내 환불요청 시 환불(재충전) 해드립니다.
(단, 단순 변심 및 실수로 인한 환불은 되지 않습니다.)
· 파일이 열리지 않거나 브라우저 오류로 인해 다운이 되지 않으면 고객센터로 문의바랍니다.
· 다운로드 받은 파일은 참고자료로 이용하셔야 하며,자료의 활용에 대한 모든 책임은 다운로드 받은 회원님에게 있습니다.
저작권안내
보고서 내용중의 의견 및 입장은 당사와 무관하며, 그 내용의 진위여부도 당사는 보증하지 않습니다.
보고서의 저작권 및 모든 법적 책임은 등록인에게 있으며, 무단전재 및 재배포를 금합니다.
저작권 문제 발생시 원저작권자의 입장에서 해결해드리고 있습니다. 저작권침해신고 바로가기