Name
Title | ||
|---|---|---|
Preface to the special issue: Isomorphisms of types and invertibility of lambda terms |
Abstract | ||
|---|---|---|
Isomorphisms of types are computational witnesses of logical equivalence with additional properties. The types/formulas A and B are isomorphic if there are functions (in a certain formalism) f : A → B and g : B → A such that g ○ f and f ○ g are equal in a certain sense to the identity on A and B, respectively. Typical such formalisms are extensions of simply typed λ-calculus, with βη-convertibility as equality relation. Another view of a pair of functions f : A → B and g : B → A (besides establishing the logical equivalence of A and B) is that f is invertible with left-inverse g, and it is then natural to relax the above symmetric condition to just g ○ f being equal to the identity on A. In this situation, A is called a retract of B, which is thus a natural generalisation of the notion of an isomorphism, while both these notions are refinements of the concept of logical equivalence in operational terms, that is, in terms of computable functions. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1017/S0960129508006798 | Mathematical Structures in Computer Science |
Keywords | Field | DocType |
computational logic,lambda calculus and related systems,polymorphism | Discrete mathematics,Logical equivalence,Retract,Generalization,Isomorphism,Formalism (philosophy),Invertible matrix,Rotation formalisms in three dimensions,Computable function,Mathematics | Journal |
Volume | Issue | ISSN |
18 | 4 | 0960-1295 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ralph Matthes | 1 | 201 | 21.67 |
| Sergei Soloviev | 2 | 100 | 14.57 |