Fundamenta Informaticae - Volume 45, issue 1-2

Authors: Girard, Jean-Yves | Urzyczyn, Paweł

Article Type: Other

Citation: Fundamenta Informaticae, vol. 45, no. 1-2, pp. i-i, 2001

Authors: Baillot, Patrick | Pedicini, Marco

Article Type: Research Article

Abstract: We introduce a geometry of interaction model given by an algebra of clauses equipped with resolution (following [10]) into which proofs of Elementary Linear Logic can be interpreted. In order to extend geometry of interaction computation (the so called execution formula) to a wider class of programs in the algebra than just those coming from proofs, we define a variant of execution (called weak execution). Its application to any program of clauses is shown to terminate …with a bound on the number of steps which is elementary in the size of the program. We establish that weak execution coincides with standard execution on programs coming from proofs. Show more

Keywords: Elementary Linear Logic, Geometry of interaction, Proof-nets, Complexity, Semantics

Citation: Fundamenta Informaticae, vol. 45, no. 1-2, pp. 1-31, 2001

Authors: Broda, Sabine | Damas, Luís

Article Type: Research Article

Abstract: We present a Counting Algorithm that computes the number of λ-terms in β-normal form that have a given type τ as a principal type and produces a list of these terms. The design of the algorithm follows the lines of Ben-Yelles' algorithm for counting normal (not necessarily principal) inhabitants of a type τ. Furthermore, we show that one can use similar algorithms with adequate limits to count normal and principal normal inhabitants in the λI-calculus.

Keywords:

Citation: Fundamenta Informaticae, vol. 45, no. 1-2, pp. 33-51, 2001

Authors: David, René

Article Type: Research Article

Abstract: This paper develops a general technique to analyze the head reduction of a term in a context. This technique is used to give a direct proof of the theorem of Hyland and Wadsworth : two λ-terms that have the same Böhm trees, up to (possibly infinite) η-equivalence, are operationally equivalent. It is also used to prove a conjecture of R. Kerth : Every unsolvable λ-term has a decoration. This syntactical result is motivated by (and gives …the solution to) a semantical problem. Show more

Keywords: λ-calculus, Böhm trees, head reduction, operational equivalence, decoration

Citation: Fundamenta Informaticae, vol. 45, no. 1-2, pp. 53-77, 2001

Authors: Sato, Masahiko | Sakurai, Takafumi | Burstall, Rod

Article Type: Research Article

Abstract: We introduce λε, a simply typed calculus with environments as first class values. As well as the usual constructs of λ and application, we have e[a] which evaluates term a in an environment e. Our environments are sets of variable-value pairs, but environments can also be computed by function application and evaluation in some other environments. The notion of environments here is a generalization of explicit substitutions and records. We show that the calculus has desirable …properties such as subject reduction, confluence, conservativity over the simply typed λβ-calculus and strong normalizability. Show more

Keywords: explicit environments, simply typed calculus, confluence, conservativity, strong normalizability

Citation: Fundamenta Informaticae, vol. 45, no. 1-2, pp. 79-115, 2001

Authors: Statman, Rick

Article Type: Research Article

Abstract: In 1975, G. Jacopini proved the existence of an easy term, i.e., a term which can be consistently (with beta conversion) identified with any other term. In 1980, A. Visser generalized Jacopini's result to R.E. theories; namely, easy terms for consistent (with beta conversion) R.E. theories exist. Of course, no such generalization for non-R.E. theories exists. For example, it is easy to see that there is no easy term for Barendregt's theory H. In this note …we shall generalize Jacopini's result to non-R.E. theories as follows. Say that an equation M=N is easy if for any consistent (with beta conversion) extension T we have that T∪{M=N} is consistent. We shall prove that easy equations exist. Show more

Keywords: Lambda calculus, consistency

Citation: Fundamenta Informaticae, vol. 45, no. 1-2, pp. 117-121, 2001

Authors: Urban, C. | Bierman, G.M.

Article Type: Research Article

Abstract: In this paper we present a strongly normalising cut-elimination procedure for classical logic. This procedure adapts Gentzen's standard cut-reductions, but is less restrictive than previous strongly normalising cut-elimination procedures. In comparison, for example, with works by Dragalin and Danos et al., our procedure requires no special annotations on formulae and allows cut-rules to pass over other cut-rules. In order to adapt the notion of symmetric reducibility candidates for proving the strong normalisation …property, we introduce a novel term assignment for sequent proofs of classical logic and formalise cut-reductions as term rewriting rules. Show more

Keywords: Classical Logic, Cut-Elimination, Strong Normalisation, Symmetric Reducibility Candidates

Citation: Fundamenta Informaticae, vol. 45, no. 1-2, pp. 123-155, 2001