This question concerns Bart Jacobs' paper "Simply typed and untyped Lambda Calculus revisited", in "Applications of Categories in Computer Science", Durham Proceedings, London Mathematical Society Lecture Note Series No. 177 In Example 3.2, Bart Jacobs constructs a term model for a certain kind of fibration (or indexed category). The base category has contexts as objects, i.e., finite tuples of type declarations, while morphisms are finite tuples of (beta-eta-equivalence classes of) terms. I have some trouble seeing that this category has finite products, given by concatenation of contexts, as claimed. Unless each variable can only be used once, isn't it possible to overwrite a declaration x:tau by x:sigma in a different context? This seems to make concatenation nonsymmetric (and one loses the projections as well). Computer Scientists here tell me that the ability to overwrite type declarations is essential for their work. I don't know whether Bart Jacobs has access to the net; maybe someone can forward this question to him? Thank you. regards, J"urgen -- J"urgen Koslowski | If I don't see you no more in this world Department of Mathematics | I meet you in the next world Kansas State University | and don't be late! koslowj@math.ksu.edu | Jimi Hendrix (Voodoo Chile) ==============================================================================
Unless each variable can only be used once, isn't it possible to overwrite a declaration x:tau by x:sigma in a different context? This seems to make concatenation nonsymmetric (and one loses the projections as well). Computer Scientists here tell me that the ability to overwrite type declarations is essential for their work. I haven't read the paper in question but I can comment on this. In most presentations of typed \lambda calculi (e.g. Barendregt's PTS) this case (repeated use of the same variable) is excluded. Indeed it does not matter for the expressibility of the system because we can always consistently rename variables (\alpha conversion). Actually I prefer to use deBruijn indizes anyway. The translation of named variables into those indizes is certainly a matter for people writing compilers (i.e. handling a symbol table) but it should not be confused with the \lambda calculus. This two issues can and should be treated completeley seperately. DeBruijn indizes precisely correspond to projections and the usual operations of substitution and weakening have nice categorical explanations. Named variables are a complete redherring. Thorsten Altenkirch And there's a hand, my trusty fiere, Laboratory for Foundations And gie's a hand o' thine, of Computer Science And we'll tak a right guid-willie waught University of Edinburgh For auld lang syne! ==============================================================================
Reply to a question by J"urgen Koslowski (from 26 Oct 92). In logic and type theory, variables are there for human convenience. They are just pointers, which are given names. Such names are often used `locally' (i.e. in a specific term or formula) with an implicit convention that there are no `global' name clashes. Category theory provides a variable-free formalism for logics and type theories. One uses projections instead of variables. Things become more precise, but less readable. In constructing categories from syntax (as I did in Example 3.2 of my Durham 1991 paper in LMS 177, to which J"urgen refers), one can either use a very precise syntax (e.g. with de Bruijn indices) or be very sloppy and hope the reader is willing to understand things in the appropriate way. Clearly I have chosen the latter approach. Below is a syntax for variables and contexts in simply typed lambda calculus, which solves the problems mentioned by J"urgen. It is not the syntax which is used in practice, but it is still readable. I'll use semi-LaTeX and write the letters `s' and `t' for types \sigma and \tau and `G' and `D' for contexts \Gamma and \Delta. Fix an infinite set Var = {v_1, v_2, v_3,...} of variables. A context is defined to be a finite sequence of types written as G = v_1:s_1, ..., v_n:s_n where by convention one counts the variables starting from 1. Assume another context D = v_1:t_1, ..., v_m:t_m then the concatenation G,D is defined to be G,D = v_1:s_1, ..., v_n:s_n, v_n+1:t_1, ..., v_n+m:t_m In this way no variable clashes occur (and hence no overwriting). The projections are the (equivalence classes of the) sequences (v_1,...,v_n) : G,D --> G (v_n+1,...,v_n+m) : G,D --> D This makes G,D the cartesian product of contexts G and D in the base category of contexts in Example 3.2 in loc. cit. I assume J"urgen now wants to know the rules for handling such `canonical contexts'. Here they are. PROJECTION ---------------- v_1:s |- v_1:s WEAKENING G |- M:t ---------------- G,v_n:s |- M:t (where G is supposed to be of length n-1) CONTRACTION G,v_n:s,v_n+1:s |- M:t --------------------------- G,v_n:s |- M[v_n/v_n+1]:t EXCHANGE G,v_i:s_i,v_i+1:s_i+1,D |- M:t ----------------------------------------------------- G,v_i:s_i+1,v_i+1:s_i,D |- M[v_i/v_i+1,v_i+1/v_i]:t Using such a precise syntax the problem raised by J"urgen can be solved. I did not put it in the paper because I thought it would distract too much. Bart Jacobs. Address since Aug.1, 1992: Mathematical Institute, RUU P.O.Box 80.010 3508 TA Utrecht The Netherlands Email: bjacobs@math.ruu.nl ==============================================================================
participants (3)
-
alti＠dcs.ed.ac.uk -
bjacobs＠math.ruu.nl -
koslowj＠math.ksu.edu