Abstract Following the Crisis of Foundations Hilbert proposed to consider a finitistic form of arithmetic as mathematics’ safe core. This approach to finitism has often admitted primitive recursive function definitions as obviously finitistic, but some have advocated the inclusion of additional variants of recurrence, while others argued that, to the contrary, primitive recursion exceeds finitism. In a landmark essay, William Tait contested the finitistic nature of these extensions, due to their impredicativity, and advocated identifying finitism with primitive recursive arithmetic, a stance often referred to as Tait’s Thesis. However, a problem with Tait’s argument is that the recurrence schema has itself impredicative and non-finitistic facets, starting with an explicit reference to the functions being defined, which are after all infinite objects. It is therefore desirable to buttress Tait’s Thesis on grounds that avoid altogether any trace of concrete infinities or impredicativity. We propose here to do just that, building on the generic framework of [ 13]. We provide further evidence for Tait’s Thesis by outlining a proof of a purely finitistic version of Parsons’ theorem, whose intuitive gist is that finitistic reasoning is equivalent to finitistic computing.

Abstract Recurrence can be used as a function definition schema for any nontrivial free algebra, yielding the same computational complexity in all cases. We show that primitive-recursive computing is in fact independent of free algebras altogether, and can be characterized by a generic programming principle, namely the control of iteration by the depletion of finite components of the underlying structure.

The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2017 edition of the award.

Common data-types, such as N, can be identified with term algebras. Thus each type can be construed as a global set; e.g. for N this global set is instantiated in each structure S to the denotations in S of the unary numerals. We can then consider each declarative program as an axiomatic theory, and assigns to it a semantic (Curry-style) type in each structure. This leads to the intrinsic theories of [Leivant, 2002], which provide a purely logical framework for reasoning about programs and their types. The framework is of interest because of its close fit with syntactic, semantic, and proof theoretic fundamentals of formal logic. This paper extends the framework to data given by coinductive as well as inductive declarations. We prove a Canonicity Theorem, stating that the denotational semantics of an equational program P, understood operationally, has type \tau over the canonical model iff P, understood as a formula has type \tau in every "data-correct" structure. In addition we show that every intrinsic theory is interpretable in a conservative extension of first-order arithmetic.

We establish a match between two broad approaches to reasoning about programs: modal (dynamic logic) proofs on the one hand, and explicit higher-order reference to program semantics, on the other. We show that Pratt-Segerberg's first-order dynamic logic DL proves precisely program properties that are provable in second-order logic with set-existence restricted to a natural class of formulas, well-known to be related to computation theory. The set-existence principle is for computational formulas, i.e. of the form forallRexistxoarrF where R is relational, F quantifier-free. Depending on the exact nature of the programs considered, some fine tuning is needed. We establish a descriptive match, of independent interest, between programming languages L and particular classes DL of computational formulas, in the following sense: the semantics of programs alphaisinL is explicitly definable, in all relational structures, by a formula phialphaof DL; and for every formula phi of DLthere is a program in L whose termination is equivalent to phi. In particular, we match the class of regular programs with random assignments to computational formulas that are "sequential", and the regular programs (without random assignments) to formulas we dub "definite", and that obey a natural variable scoping condition

Total correctness assertions (TCAs) have long been considered a natural formalization of successful program termination. However, research dating back to the 1980s suggests that validity of TCAs is a notion of limited interest; we corroborate this by proving compactness and Herbrand properties for the valid TCAs, defining in passing a new sound, complete, and syntax-directed deductive system for TCAs. It follows that proving TCAs whose truth depends on underlying inductive data-types is impossible in logics of programs that are sound for all structures, such as dynamic logic based on Segerberg's PDL, even when augmented with powerful first-order theories like Peano arithmetic. Harel's convergence rule bypasses this difficulty, but is methodologically and conceptually problematic, in addition to being unsound for general validity. We propose instead to bind variables to inductive data via DL's box operator, leading to an alternative formalization of termination assertions, which we dub inductive TCA (ITCA). We observe that a TCA is provable in Harel's DL exactly when the corresponding ITCA is provable in Segerberg's DL, thereby showing that the convergence rule is not foundationally or practically necessary. We also show that validity of ITCAs is directly reducible to validity of partial correctness assertions, confirming the foundational importance of the latter.

We characterize computationally the functions provable in second order logic with set existence restricted to natural classes of first order formulas. A classification of first-order set-existence by implicational rank yields a natural hierarchy of complexity classes within the class of Kalmar-elementary functions: The functions over {0, 1}* constructively provable using set existence for formulas of implicational rank /spl les/k are precisely the functions computable in deterministic time O(exp/sub k/(n)), where exp/sub 0/=U/sub k/(/spl lambda/n.n/sup k/), and exp/sub k+1/=2(exp/sub k/)./sup 1/ In particular, set-existence for positive formulas yields exactly PTime. We thus obtain lean and natural formalisms for codifying feasible mathematics, which are expressive both in allowing second order definitions and reasoning, and in incorporating equational programming and reasoning about program convergence in a direct and uncoded style. Through a formula-as-type morphism, we also obtain a link with lambda definability, which we exhibit in the full paper: The functions over {0, 1}* definable in the polymorphic lambda calculus F/sub 2/ over a base of type of words, using first-order type-arguments of rank /spl les/k, are precisely the functions computable in deterministic time O(exp/sub k/(n))./sup 2/ The poly-time case was proved (directly) in [15].

We show that a boolean valued function is in NC if it is defined by ramified schematic recurrence over trees. This machine-independent characterization uses no initial functions other than basic tree operations, and no bounding conditions on the recurrence. Aside from its technical interest, our result evidences the foundational nature of NC, thereby illustrating the merits of implicit (i.e. machine independent) computational complexity theory.

No abstract available.

We develop two notions of stratified recur-1 introduction rence.The first is predicative recurrence, and is similar to

A principle directly pertinent to feasibility, which justifies the identification of P-time with feasible computing, is proposed. It is shown that the computable functions justified on the basis of positive quantifier-free comprehension are precisely the functions computable in deterministic polynomial time. This shows that the class P-time arises naturally from a foundational analysis of feasibility, and that terms using exponentiation can be justified as meaningful only under the admission of infinite sets as completed totalities.>

The author considers a spectrum of predicative type abstraction disciplines based on type quantification with stratified levels. These lie in the vast middle ground between parametric abstraction and full impredicative abstraction. Stratified polymorphism has an attractive, unproblematic semantics, and has the potential of offering new approaches to type inference, without sacrificing useful expressive power. He shows that the functions representable in the finitely stratified lambda -calculus are precisely the superelementary functions, i.e., E/sub 4/ in A. Grzegorczyk's (Rozprawy Mate. IV, Warsaw, 1953) subrecursive hierarchy. He also defines methods of transfinite stratification and shows that stratification up to omega /sup omega / has a simple finitary representation, making it a potentially useful concept in programming language design. The author proves that the functions represented by stratified polymorphism up to omega /sup omega / are precisely the primitive recursive functions. He points out that these results imply that the equality problem for finitely stratified lambda -calculus is not superelementary, and that the equality problem for the calculus stratified up to omega /sup omega / is not primitive recursive.>

The nature of programming languages that fail to have a relatively complete proof formalism is discussed. First, it is shown that such failures may be due to the meagerness of the programming language, rather than to the presence of complex control structures as in the cases studied so far. The failure of relative completeness is then derived for two languages with a rich control structure, using simple simulations of general recursive functions by procedure call mechanisms.

The notion of relative completeness of logics of programs was delineated almost ten years ago, in particular by Wand, Cook and Clarke. More recently, it has been felt that Cook's notion hinges on a fragile balance between the semantics of a programming language and first-order expressiveness in structures. This fragility underlies the negative results about relative completeness.

Logical and mathemlicnl reasoning ahout impcrdtive programs.'

Syntactic translations of classical logic C into intuitionistic logic I are well known (see [Kol25], [Gli29], [Göd32], [Kre58b], [M063], [Cel69] and [Lei71]). Harvey Friedman [Fri78] used a translation of a similar nature, from I into itself, to reprove a theorem of Kreisel [Kre58a] that various theories based on I are closed under Markov's rule: if ¬¬∃x.α is a theorem, where x is a numeric variable and α is a primitive recursive relation, then ∃x.α is a theorem. Composing this with Gödel's translation from classical to intuitionistic theories, it follows that the functions provably recursive in the classical version of the theories considered are provably recursive already in their intuitionistic version. This conservation result is important in that it guarantees that no information about the convergence of recursive functions is lost when proofs are restricted to constructive logic, thus removing a potential objection to the use of constructive logic in reasoning about programs (see [C078] for example). Conversely, no objection can be raised by intuitionists to proofs of formulas that use classical reasoning, because such proofs can be converted to constructive proofs (this has been exploited extensively; see [Smo82]). Proofs of closure under Markov's rule had required, until Friedman's proof, a relatively sophisticated mathematical apparatus. The chief method used Godel's “Dialectica” interpretation (see [Tro73, §3]). Other proofs used cut-elimination, provable reflection for subsystems [Gir73], and Kripke models [Smo73]. Moreover, adapting these proofs to new theories had required that the underlying meta-mathematical techniques be adapted first, not always a trivial step.

We present a method of reasoning directly about functional programs in Second-Order Logic, based on the use of explicit second-order definitions for inductively defined data-types. Termination becomes a special case of correct typing. The formula-as-type analogy known from Proof Theory, when applied to this formalism, yields λ-expressions representing objects of inductively defined types, as well as λ-expressions representing functions between such types. A proof that a functional closed expression e is of type T maps into a λ-expression representing (the value of) e; and a proof that a function f is correctly typed maps into a λ-expression representing f (modulo the representations of objects of those types). When applied to integers and to numeric functions the mapping yields Church's numerals and the traditional function representations over them. The λ-expressions obtained under the isomorphism are typed (in the Second-Order Lambda Calculus). This implies that, for functions defined over inductively defined types, the property of being proved everywhere-defined in Second-Order Logic is equivalent to the property of being representable in the Second-Order Lambda Calculus. Extensions and refinements of this result lead to other characterizations of complexity classes by type disciplines. For example, log-space functions over finite structures are precisely the functions over finite-structures definable by λ-pairing-expressions in a predicative version of the Second-Order Lambda Calculus.

The benefits of strong typing to disciplined programming, to compile-time error detection and to program verification are well known. Strong typing is especially natural for functional (applicative) languages, in which function application is the central construct, and type matching is therefore a principal program correctness check. In practice, however, assigning a type to each and every expression in a functional program can be prohibitively cumbersome. As expressions are compounded, the task of assigning a type to each expression and subexpression becomes practically impossible, even more so because the type-expressions themselves grow longer. It becomes imperative therefore to design friendly programming environments that permit the user type-free programming, but that generate fully typed programs in which the types of all expressions are inferred by the system from the program. For interactive functional programming environments of the kind implemented for the Edinburgh functional programming language ML, a type-inference system is an invaluable tool for on-line parse-time error detection and debugging.

The semantic modeling of data types has been the subject ofincreased interest over the last few years, enhanced by thedevelopment of applicative languages such as Edinburgh's ML andHOPE, by the need for flexible highly structured languages thatwould nonetheless be amenable to verification, and by ongoinginquiries on polymorphism in programming languages. In particular,there has been a growing interest in generic type structures suchas the Reynolds-Girard discipline of full polymorphism, furtherextended by McCracken [McC] and MacQueen and Sethi [MS], and inuser-defined and recursively-defined types.Our aim here is to model semantically the notion of type so asto encompass full polymorphism, but in a very controlled way whichon the one hand allows the modeling to remain simple, and on theother hand conveys as much of the notion of type as seems feasiblyrelevant to programming languages.Our leading idea is that a type is a structural condition ondata objects rather than a collection of objects which satisfiescertain closure properties. Roughly, we argue that such structuralconditions are fully conveyed by syntactic expressions, not inisolation of course, but within a syntax-oriented typediscipline. In other words, we treat types as discrete objects,which merely code the ways data objects are allowed to interact (asin applying functional object a to object b). Once atype discipline is set to delineate a set of type expressions, andonce the meaning of the type-constructs is imposed on the ways thedata objects relate, the meaning of each type expression isconveyed by the expression itself (reduced to a canonical form ifnecessary). This conception of types permits a strikingly simplemodeling of the use of types as arguments of data objects, a usecentral to Reynolds' polymorphic type system [Rey].The use of types as genuine arguments of procedures is notdevoid of practical interest. E.g., one may wish to treat objectsof type o generically, except for an initial choice dependingon the principal type-constructor of o, that is, according towhether o is an atomic type, a functional type, a cartesianproduct, etc.A particular situation where such choices may be useful is wherea procedure has a formal parameter intended to range over some datastructure (trees of sequences of objects of type t, say), adata structure that has a number of accepted representations byformal data types. It seems desirable to permit the definition of apolymorphic procedure that would accept as valid a number of suchformal representations, branching on them internally. This kind offacility would elevate the polymorphism of a procedure from thelevel of uses with in a single program, to the level oftransportability from one set of data structure specifications toanother.This kind of use of types as arguments is compatible withReynold's discipline of type abstraction, but not with thequantificational discipline of [MS] (cf.[Lei83], §4.2). Whilethe two disciplines, as uninterpreted and unexpanded calculi, arecombinatorially isomorphic the difference between their intendedsemantics becomes apparent when primitive functions over types(such as discriminators over main type-constructor) areconsidered.The examples we have given of uses of types as arguments arefairly restricted in nature: all that is used of a type is itssyntactically representable structure. This is not merely anempirical observation on our limited perception at present time. Ina typed discipline of programming each object carries its type(explicitly or not), and all types of denotable objects arethemselves denotable. It follows that any question that one may askabout the type of a denotable object reduces to a question abouttype-expression(s) denoting that type. The issue of semanticallymodeling Reynold's rich discipline of type abstraction is thereforereduced, from a pragmatic point of view, to a modeling in whichquestions about types are all expressible as questions about typeexpressions.Existing approaches to the semantic modeling of data types are,in one form or another, conceptual continuations of thedenotational semantics approach to data objects. McCracken [McC],following [Sco], defines types as retracts of the universal domain.In Shamir and Wadge [SW], Milner [Mil] and MacQueen and Sethi [MS]types are modeled as some kind of ideal, where an ideal is asubset of the object-domain that satisfies certain closureconditions. In both approaches types are being defined via theproperties that they must satisfy, as sets of objects, so as tobecome compatible with their use. (This may be compared with thealgebraic approach to types, where each particular type isdefined via its algebraic properties rather than its intendedconception).Our modeling of types too is grafted on top of a denotationalsemantics for the object language, However,it has a life of itsown, and can be explained in isolation, or combined with forinstance, an operational semantics for the object language. Thepoint we are trying to make is that the semantics of types haslittle to do with the issues of self-application and continuitywhich motivate denotational semantics. Rather than amalgamateobjects and types, as in [SW] (where types as sets of objects aretreated on an equal footing with objects as sets ofapproximations), we separate the two radically.We make no claim, of course, that our approach should supplantthe modeling of types as retracts or as ideals. Rather, we believethat the semantics we propose is related to types-as-ideals in muchthe same way as operational semantics is related to denotationalsemantics: it is closer to programming practice, permits a smallerset of objects, and is sensitive to the choice of formal framework(which for us is the type discipline). We therefore feel that thetwo approaches should shed light on each other and, in combination,enhance our understanding of complex data-types and and theirproper use.In particular, we believe that even putting down the definitionsand proving basic existence theorems provides some insight aboutthe design and use of data types. For one, our modeling of typessuggests a feasible controlled use of types as arguments of dataobjects. For another, it points to directions in setting very richtype disciplines evolving naturally from a structural-computationalview of types. For instance, it may be useful and feasible toconsider types built as certain recursive sets of other types.Following preliminaries in sections 1 and 2 we define in section3 what is a model of the pure polymorphic lambda calculus.A termmodel is constructed in §4,in §5 we show how to constructa non-extensional model through the solution of a domain equation,and in §6 we construct an extensional model through such asolution. The latter construction involves breaking the circularityin the conditions underlying polymorphic typing, by a method akinto Girard's in the proof theory of higher order logic [Gir].We plan to extend this work in two directions. One is thetreatment of more general type disciplines, of the kinds defined byMcCracken [McC] and further studied by MacQueen and Sethi [MS]. Thecrucial issue here is that, in contrast to Reynold's discipline,distinct type expressions may denote the same type. However, eachtype expression has a normal form, which may be viewed as itsvalue (this view has been advocated in greater generality by PerMartin-Lof [Mar], on somewhat more philosophical grounds). A seconddirection, incorporating aspects of the first, is the treatment ofrecursively defined data types in a polymorphic context, andpossibly more general notions of types.

Typed lambda (?`-) calculi provtde convement mathematical settings in which to investigate the effects of type structure on the function definmon mechamsm m programming languages.Lambda expressaons mtm~c programs that do not use while loops or carcular function definitions.Two typed ?`-calculi are investigated, the sunply typed ?`-calculus, whose types are similar to Pascal types, and the second-order typed ?,-calculus, which has a type abstractaon mechamsm simdar to that of modern data abstraction languages such as ALPHARD.Two related questions are considered for each calculus: (1) What functaons are definable m the calculus?and (2) How difficult is the proof that all expressions in the calculus are normahzable 0.e., that all computaUons termmate)* The simply typed calculus only defines elementary functtons.Normahzation for this calculus ~s provable using commonplace forms of reasoning formalazable m Peano arithmetic The second-order calculus defines a huge hierarchy of funcuons going far beyond Ackermann's function These funcuons are so rapidly increasing that Peano arithmetic cannot prove that they are total In fact, normalizataon for the second-order calculus cannot be proved even m second-order Peano artthmetic, nor m Peano anthmettc augmented by all true statements Also d~scussed are the lmphcataons of the present ?`-calculusresults for the programming languages PASCAL, ALPHARD, RUSSELL, and MODEL.

By induction for a formula φ we mean the schema (where the terms in brackets are implicitly substituted for some fixed variable, with the usual restrictions). Let be the schema IAφ for φ in Πn (i.e. ); similarly for . Each instance of is Δn+2, and each instance of is Σn+1 Thus the universal closure of an instance α is Πn+2 in either case. Charles Parsons [72] proved that and are equivalent over Z0, where Z0 is essentially Primitive Recursive Arithmetic augmented by classical First Order Logic [Parsons 70]. Theorem. For each n > 0 there is a Πn formula π for which is not derivable in Z0from (i) true Πn+1sentences; nor even (ii) Πn+1sentences consistent withZ0.

Our subject is at the confluence of two foundational research areas: formal independence results, and higher order data types.

In classical arithmetic a natural measure for the complexity of relations is provided by the number of quantifier alternations in an equivalent prenex normal form. However, the proof of the Prenex Normal Form Theorem uses the following intuitionistically invalid rules for permuting quantifiers with propositional constants. Each one of these schemas, when added to Intuitionistic (Heyting's) Arithmetic IA, generates full Classical (Peano's) Arithmetic. Schema (3) is of little interest here, since one can obtain a formula intuitionistically equivalent to A ∨ ∀xBx, which is prenex if A and B are: For the two conjuncts on the r.h.s. (1) may be successively applied, since y = 0 is decidable. We shall readily verify that there is no way of similarly going around (1) or (2). This fact calls for counting implication (though not conjunction or disjunction) in measuring in IA the complexity of arithmetic relations. The natural implicational measure for our purpose is the depth of negative nestings of implication, defined as follows. I(F): = 0 if F is atomic; I(F ∧ G) = I(F ∨ G): = max[I(F), I(G)]; I(∀xF) = I(∃xF): = I(F); I(F → G):= max[I(F) + 1, I(G)].

The modal logic GL has been found by Solovay [13] to formalize the provable propositional properties of the provability-predicate for Peano's Arithmetic PA (cf. §1 below). We give several sequential calculi for GL, compare their merits, and use one calculus to syntactically derive several metamathematical results about GL. Some of our results have been proved model theoretically, and similar proofs are fairly straightforward for several of the remaining ones (G. Boolos and the referee have provided such proofs for 4.1, 4.3 and 5.1 below). However, our syntactic techniques often yield more concise and obviously constructive proofs, they offer additional insight into the nature of the systems considered, and are easily adaptable to systems for which semantical analysis is problematic. I am indebted to G. Boolos and to the referee for their valuable advice. The referee has suggested the rule GL of §3 below as an axiomatization of GL; the resulting sequential calculus has allowed a definite improvement of our original presentation.

In classical first-order predicate logic CL1 (without equality) only tautologies and antitautologies satisfy nontautological schemas. I.e., if F[p, Q] is a nontautological formula (fl) in the predicate letters shown, with p prepositional, then ⊬ F[K, Q] for any sentence K not containing some Q ∈ Q, unless ⊢ K or ⊢ ¬K. This is an easy consequence of the Completeness Theorem. Clearly, the analogous statement fails for intuitionistic predicate logic IL1; already when Q is empty: (i) ¬¬ K for, e.g., K ≡ p ∨ ¬p; (ii) ¬¬K → K for, e.g., K ≡ ¬p.