On Implicit Arguments

A typechecker for a typed -calculus having implicit arguments is presented. The typechecker works in such a way that the uniqueness of implicit arguments is always preserved during reduction. Consequently, when it compares two terms by reduction, it can reduce them without inferring implicit arguments. Before describing the typechecker, we analyze various situations where the uniqueness of implicit arguments is not preserved by naively defined reduction. ANY OTHER IDENTIFYING INFORMATION OF THIS REPORT The preliminary version of this paper appeared in Logic, Language and Computation, Lecture Notes in Computer Science, Vol.792, 1994, pp.10-30. DISTRIBUTION STATEMENT First issue 40 copies. This technical report is available via anonymous FTP from ftp.is.s.u-tokyo.ac.jp (directory /pub/tech-reports). SUPPLEMENTARY NOTES REPORT DATE January 1, 1995 TOTAL NO. OF PAGES 31 WRITTEN LANGUAGE English NO. OF REFERENCES 12 DEPARTMENT OF INFORMATION SCIENCE Faculty of Science, Universit..