This is written from the point of view of someone who would like to see a computational system which is much nearer to real mathematics than the current widely used systems (Maple, Mathematica, and various more specialised systems, e.g. Singular). Of these the only one which is clearly typed is Singular. There is also AXIOM, which has parametrised types, types can be variables, there is multiple inheritance and coercion. It looks much nearer to what should be mathematics. On the other hand, its literature does not include any theory of the type system, so consistency is not clear, and it is not generally used. So my question is: does all this general theory of types give a clear indication as to what should be, not necessarily a final, but certainly a convenient theory adequate for expressing a majority of present day maths? Let's make up a test case: one should be able to code reasonably conveniently the type of a general groupoid acting on exterior algebras over a commutative ring, and also of course the category of such objects. A groupoid acting on exterior algebras with zero multiplication should be coercible to a groupoid acting on graded modules. I would prefer the sytem to be so simple that it will allow tests for consistency of new proposed types. Also it should be easy to understand, since it would represent nicely current practice. Is this idea a mirage? Ronnie On Thu, 18 Mar 1999, R.A.G. Seely wrote:
My 1987 JSL paper is a start - "Categorical Semantics for Higher-Order Polymorphic Lambda Calculus", JSL 52 (1987) 4, pp 969 - 989. In particular, look at section 3, where the model of closure operators is described in categorical terms.
= rags =
On Thu, 18 Mar 1999, Elaine Gouvea Pimentel wrote:
I'd like to know if there is any categorical model for polymorphic lambda-calculus.
================================= <rags@math.mcgill.ca> <http://www.math.mcgill.ca/~rags>
Prof R. Brown, School of Mathematics, University of Wales, Bangor Dean St., Bangor, Gwynedd LL57 1UT, United Kingdom Tel. direct:+44 1248 382474|office: 382475 fax: +44 1248 383663 World Wide Web: home page: http://www.bangor.ac.uk/~mas010/ New article: Higher dimensional group theory Symbolic Sculpture and Mathematics: http://www.bangor.ac.uk/SculMath/ Mathematics and Knots: http://www.bangor.ac.uk/ma/CPM/exhibit/welcome.htm