Skip to Main content Skip to Navigation
Journal articles

Sequent combinators: a Hilbert system for the lambda calculus

Abstract : This paper introduces Hilbert systems for λ-calculus, called sequent combinators, addressing many of the problems of Hilbert systems that have led to the more widespread adoption of natural deduction systems in computer science. This suggests that Hilbert systems, with their uniform approach to meta-variables and substitution, may be a more suitable framework than λ-calculus for type theories and programming languages. Two calculi are introduced here. The calculus SKIn captures λ-calculus reduction faithfully, is confluent even in the presence of meta-variables, is normalizing but not strongly normalizing in the typed case, and standardizes. The sub-calculus SKInT captures λ-reduction in slightly less obvious ways, and is a language of proof-terms not directly for intuitionistic logic, but for a fragment of S4 that we name near-intuitionistic logic. To our knowledge, SKInT is the first confluent, first-order calculus to capture λ-calculus reduction fully and faithfully and be strongly normalizing in the typed case. In particular, no calculus of explicit substitutions has yet achieved this goal.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/hal-03207821
Contributor : Jean Goubault-Larrecq <>
Submitted on : Monday, April 26, 2021 - 10:38:19 AM
Last modification on : Wednesday, April 28, 2021 - 3:11:05 AM

Identifiers

Collections

Citation

Healfdene Goguen, Jean Goubault-Larrecq. Sequent combinators: a Hilbert system for the lambda calculus. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2000, 10 (1), pp.1-79. ⟨10.1017/S0960129599002911⟩. ⟨hal-03207821⟩

Share

Metrics

Record views

8