Reflections on the Foundations of Meta-Programming: Is a Type Theory Needed?

bryöecrc.de Meta-programming is an important programming technique, which is widely applied in logic pro gramming- cf. e.g. [1,2,3,4,5,6]. However, in spite of several studies- cf. e.g. [28,29,30]- the semantics of meta-programs and their formalization in logic remain open issues. Formalizations in classical logic, such as that subjacent to the Gödel language [31], are in the spirit of the classical formalization of first-order programs- cf. e.g. [8,9]. They interpret meta-predicates and predicate variables as higher-order symbols. How attractive they might be, the formalizations in classical logic are not conform to a programmer's intuition. Moreover, although such approaches rather con vincingly formalize constructs such as Prolog "call " and "clause " l they generally fail to account for constructs permitting a dynamic creation of predicate symbols and atoms, such as Prolog "univ" (=..) , "functor", and "arg ". The formalizations of meta-programming based on many-sorted logics, e.g. [10], are more intuitive. Nevertheless, they also fail to explain the dynamic creation of symbols. We argue that the inadequacy of classical logic to formalize meta-programming is related to the theory of types of this logic, i.e. to the principles that were introduced first by Russel in [ l l]. 1 We argue that the standard models of meta-programs viewed as higher-order theories i