DSpace About DSpace Software

Kyushu Institute of Technology Academic Repository(Kyutacar) >
03. 紀要・テクニカルレポート = Bulletin・Technical Report >
テクニカルレポート  >

Please use this identifier to cite or link to this item: http://hdl.handle.net/10228/933

Title: Type Inference for Domain-Free λ2
Authors: Fujita, Ken-etsu
Department of Articial Intelligence,Kyushu Institute of Technology
九州工業大学情報工学部 知能情報工学科
藤田, 憲悦
Issue Date: 1-Jul-1999
Publisher: 九州工業大学
Abstract: We will prove that type checking, typability, and type inference for domain-free 2 are undecidable. The type checking problem for domain- free 2 was posed by Barthe and S rensen (1997). A certain second or- der uni cation problem is reduced to the problem of type inference for domain-free 2. The restricted second order uni cation has been proven undecidable by Schubert. The reduction method can be obtained from a simpli cation of Pfenning's reduction from the general problem of second order uni cation to the partial type inference problem. An analysis of the undecidability proof reveals that the typability problem is still undecid- able even for a predicative fragment of domain-free 2, called the rank 2 fragment.
URI: http://hdl.handle.net/10228/933
Appears in Collections:テクニカルレポート

Files in This Item:

File Description SizeFormat
csse5.pdf184.73 kBAdobe PDFView/Open

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.


Valid XHTML 1.0! DSpace Software Copyright © 2002-2007 MIT and Hewlett-Packard - Feedback