Del 3 al 7 de Noviembre, se realizará en el State Key Laboratory del Institute for Software de la Chinese Academy of Science, en Beijing, un workshop del projecto Franco-Chino LOCALI. Allí voy a presentar una charla. Les dejo aquí abajo el título y resumen.
Título: Identificando proposiciones isomorfas
Resumen:
En lambda-cálculo tipado, en lenguajes de programación y en teoría de la prueba, dos tipos
y 
se dicen isomorfos, si existen dos funciones 
y 
tales que 
, y 
. En algunos casos, los tipos isomorfos son considerados iguales. Por ejemplo en teoría de tipos de Martin-Löf, en Cálculo de Construcciones y en Deducción módulo, tipos iguales por definición son identificados. Sin embargo, igualdad por definición es mas débil que isomorfismo y, por ejemplo, los tipos isomorfos 
y 
usualmente no son identificados: un término de tipo no tiene tipo .
No identificar esos tipos tiene muchos inconvenientes, por ejemplo si una biblioteca contiene una prueba de, una llamada a una prueba de no podrá encontrarla, si 
y 
son pruebas de \Rightarrow C "(A\wedge B)\Rightarrow C")
y respectivamente, no es posible aplicar a para obtener una prueba de 
, necesitamos explícitamente aplicar una función de tipo\Rightarrow (A\wedge B) "(B\wedge A)\Rightarrow (A\wedge B)")
a antes de aplicar a este término. Esto ha llevado a un auge de proyectosde investigación con el objetivo de identificar de una forma u otra tipos isomorfos en teoría de tipos, por ejemplo con el axioma de univalencia.
Aquí introducimos una extensión de lambda cálculo simplemente tipado con pares, donde tipos isomorfos son identificados. En este cálculo nos enfocamos en tres isomorfismos: conmutatividad y asociatividad de la conjunción, y distributividad de la implicación sobre la conjunción. Identificar tipos requiere también identificar términos via una relación de equivalencia, lo cual deriva en un cálculo interesante, relacionado con varios cálculos algebraicos y no deterministas conocidos. En esta charla voy a presentar el sistema y una prueba de normalización basada en una adaptación no trivial de la técnica de candidatos de reducibilidad. Además, voy a mostrar algunas ideas en progreso para intruducir la currificación:\Rightarrow C \equiv A\Rightarrow B\Rightarrow C "(A\wedge B)\Rightarrow C \equiv A\Rightarrow B\Rightarrow C")
.
Título: Identificando proposiciones isomorfas
Resumen:
En lambda-cálculo tipado, en lenguajes de programación y en teoría de la prueba, dos tipos
No identificar esos tipos tiene muchos inconvenientes, por ejemplo si una biblioteca contiene una prueba de
Aquí introducimos una extensión de lambda cálculo simplemente tipado con pares, donde tipos isomorfos son identificados. En este cálculo nos enfocamos en tres isomorfismos: conmutatividad y asociatividad de la conjunción, y distributividad de la implicación sobre la conjunción. Identificar tipos requiere también identificar términos via una relación de equivalencia, lo cual deriva en un cálculo interesante, relacionado con varios cálculos algebraicos y no deterministas conocidos. En esta charla voy a presentar el sistema y una prueba de normalización basada en una adaptación no trivial de la técnica de candidatos de reducibilidad. Además, voy a mostrar algunas ideas en progreso para intruducir la currificación:
From the 3rd to the 7th of November, a workshop of the ANRI LOCALI Project will take place at the State Key Laboratory of the Institute for Software of the Chinese Academy of Science, in Beijing. I will give a talk there. Below you will find the title and abstract of it.
Title: Identifying isomorphic propositions
Abstract:
In typed lambda-calculus, in programming languages, and in proof theory, two types and are said to be isomorphic, if there exists two functions and such that , and . In some cases, isomorphic types are identified. For instance, in Martin-Löf's type theory, in the Calculus of Constructions, and in Deduction modulo, definitionally equivalent types are identified. However, definitional equality is weaker than isomorphism and, for example, the isomorphic types and are not usually identified: a term of type does not have type .
Not identifying such types has many drawbacks, for example if a library contains a proof of, a request on a proof of fails to find it, if and are proofs of and respectively, it is not possible to apply to to get a proof of , but we need to explicitly apply a function of type to before we can apply to this term. This has lead to several projects aiming to identify in a way or another isomorphic types in type theory, for example with the univalence axiom.
We introduce an extension of simply typed lambda calculus with pairs where isomorphic types are identified. In this calculus we have focused on three isomorphisms: associativity and commutativity of conjunction, and the distributivity of implication over conjunction. Identifying some types requires to also identify some terms via an equivalence relation on terms, leading to an interesting calculus, which is related to several known algebraic and non-deterministic calculi. In this talk I will present the system and a proof of normalisation based on a non-trivial adaptation of the reducibility candidates technique. Also I will show some ongoing ideas to introduce the curryfication:.
Title: Identifying isomorphic propositions
Abstract:
In typed lambda-calculus, in programming languages, and in proof theory, two types
Not identifying such types has many drawbacks, for example if a library contains a proof of
We introduce an extension of simply typed lambda calculus with pairs where isomorphic types are identified. In this calculus we have focused on three isomorphisms: associativity and commutativity of conjunction, and the distributivity of implication over conjunction. Identifying some types requires to also identify some terms via an equivalence relation on terms, leading to an interesting calculus, which is related to several known algebraic and non-deterministic calculi. In this talk I will present the system and a proof of normalisation based on a non-trivial adaptation of the reducibility candidates technique. Also I will show some ongoing ideas to introduce the curryfication:
Update: The slides
