Download xaut021.pdf

Contents : M ATHEMATICAL CENTRE TRACTS 1 60 ABSTRACT AUTOMATH A . REZUS MATH EMATISCH CENTRUM AMST E D A M 1983 W 1980 Mathematics subject classification: Primary: 03B40 Secondary: 03-04 03F99 68-04 68C20 ISBN 9 0 6196 256 0 c o p y r i g h t O 1983 Mathematisch Centrum Amsterdam "De objectiveering der wereld in wiskundige systemen b j verschillende individui en wordt in onderling verband gehouden door de passielooze taa1 die bi den hoorder het identieke wiskundige sssteem als b j den spreker doet oprijzeh terwijl de i gevoelsinhoud van dat systeem b j beiden i totaal verschillend kan zijn (L.E.J.BROUWER: "Wiskunde en Ervaring".) . .." P R E F A C E The idea of a computer-assisted proof-checking (applied to concrete proofs as they appear in the mathematician's everyday life) has probably occurred to many mindsteven before the von Neumann computer was conceived. In particular an attempt to increase the reliability of mathematical texts (proofs) by having them processed and checked on computer has also been the main motivation behind the specific AUTOmated MATHematics Project developed since 1967 at the Eindhoven University of Technology. Abstracting from the pragmatic motivations (cf. 02. below) a sufficiently complex AUTOMATH-system (the "classical" version: AUT-68 say) can beviewed as an (applied) typed lambda-calculus with a "polymorphic" type-structure (to coin a word from R. ilner). Although the underlying 17type-polymorphism"appears to be - at a first look - a very specific one we realize soon that an AUTOMATHsystem is powerful enough such as to allow interpreting (in it) familiar typed lambda-calculi as e.g. the Curry Theory of Functionality ( "First-order Typed Lambda-calculus") or the Girard-Reynolds Second-order ("parametric") Typed Lambda-calculus.In this respect an AUTOMATH-system is a "generalized typed lambda-calculus". At a closer examination the "pure" (i.e. constantless) part of these systems turns out to be much similar if not equivalent to other typed lambda-calculi occurring in the recent literature on the foundations of logic and mathematics.(Specifically "Pure AUT-68" is in fact a fully formalized version of J.P.Seldinls Theory of Generali-zed Functionality (cf.Annals Math.Log. 12 1979 29-59) and it becomes under an appropriate translation - equivalent to the "!-fragmentn of Martin-Lof's Theori(es) of Types (cf. 8eferences under M ABTIX-LgF'.) On the other hand the specific manipulation of the AUT(OMATH)-constants - a E & . generis feature of these systems - is up to a certain point independent from the underlying lambda-calculus part and can be used with similar effects in connection with any other typed lambda-calculus.

INFO HASH : 042923b34f1756d7d36dab3c16795b3a7ec4e2a3

Download now

File Size: 7.1 mb