From: Ronnie Brown <r.brown@bangor.ac.uk>
To: categories@mta.ca
Subject: Naive question on Polymorphic lambda-calculus, etc
Date: Fri, 19 Mar 1999 16:13:02 +0000 (GMT) [thread overview]
Message-ID: <Pine.SOL.3.90.990319154145.3087O-100000@publix> (raw)
In-Reply-To: <Pine.LNX.4.04.9903181822210.14461-100000@triples.math.mcgill.ca>
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
prev parent reply other threads:[~1999-03-19 16:13 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
1999-03-18 23:26 Polymorphic lambda-calculus R.A.G. Seely
1999-03-19 16:13 ` Ronnie Brown [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=Pine.SOL.3.90.990319154145.3087O-100000@publix \
--to=r.brown@bangor.ac.uk \
--cc=categories@mta.ca \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).