Principal types of BCK-lambda-terms
A BCK-\(\lambda\)-term is one in which each variable appears at most once. A pair \(\langle B,\alpha\rangle\) of a set of type assignments to variables \(B\) and a type \(\alpha\), is said to be a principal pair if \(B\lvdash M: \alpha'\) whenever \(\alpha'\) is a substitution instance of \(\alpha\). If \(B\) is empty (and so \(M\) is closed), \(\alpha\) is the principal type scheme of \(M\). In this paper the author gives a characterization of principal pairs for BCK-\(\lambda\)-terms using a new notion of ``connection between types in a type assignment figure. From this he is able to show that if two closed BCK-\(\lambda\)-terms in \(\beta\)-normal form have the same principal type then they are identical (modulo \(\alpha\)-conversion). A type \(\alpha\) is BCK-minimal if it is not a nontrivial substitution instance of any BCK-type. It follows that if two closed BCK-\(\lambda\)- terms in \(\beta\)-normal form have the same minimal types then these are also identical (modulo \(\alpha\)-conversion). This resolves a conjecture of Komori. By the formulas as types isomorphism, it also follows that the corresponding minimal theorems of BCK-implicational logic have unique normalized proofs.
- A theory of type polymorphism in programming
- BCK and BCI logics, condensed detachment and the 2-property
- BCK-combinators and linear \(\lambda\)-terms have types
- Coherence and valid isomorphism in closed categories applications of proof theory to category theory in a computer sclentist perspective
- Combinatory logic. Vol. II
- Combinatory logic. With two sections by William Craig.
- Condensed detachment is complete for relevance logic: A computer-aided proof
- Fully abstract models of typed \(\lambda\)-calculi
- scientific article; zbMATH DE number 4204312 (Why is no real title available?)
- scientific article; zbMATH DE number 3916223 (Why is no real title available?)
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 3668594 (Why is no real title available?)
- scientific article; zbMATH DE number 218501 (Why is no real title available?)
- scientific article; zbMATH DE number 3993540 (Why is no real title available?)
- scientific article; zbMATH DE number 3275554 (Why is no real title available?)
- Implementing the `Fool's model' of combinatory logic
- Intersection types for combinatory logic
- Linear logic
- Logics without the contraction rule
- Principal type scheme and unification for intersection type discipline
- Principal type-schemes and condensed detachment
- The Principal Type-Scheme of an Object in Combinatory Logic
- Why commutative diagrams coincide with equivalent proofs
- Über Tautologien, in Welchen Keine Variable Mehr Als Zweimal Vorkommt
- BCK-combinators and linear \(\lambda\)-terms have types
- The converse principal type-scheme theorem in lambda calculus
- On principal types of combinators
- Computing interpolants in implicational logics
- 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000. La Sorbonne, Paris, France, July 23-31, 2000
- The number of proofs for a BCK-formula
- On Principal Types of BCK-λ-Terms
- Uniqueness of normal proofs of minimal formulas
- The Relevance Graph of a BCK-Formula
- scientific article; zbMATH DE number 1497851 (Why is no real title available?)
- Studying provability in implicational intuitionistic logic: the formula tree approach
- On repetitive right application of \(B\)-terms
- Principal type-schemes of BCI-lambda-terms
- Two beta-equal lambda-I-terms with no types in common
- Most general first order theorems are not recursively enumerable
- Principal types as partial involutions
This page was built for publication: Principal types of BCK-lambda-terms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1208417)
