Cálculo lambda de primer orden con constraints y la propiedad church-rosser

Abstract

En [2,3] fue presentada una extensión al tradicional cálculo lambda con constraints. Los constraints pueden ser usados con dos distintos propósitos: en una forma pasiva, restringiendo el rango de variables, o en forma activa comput.andp soluciones a determinados sistemas. Aquí presentamos una extensión de aquél cálculo, agregándole cuantificadores existenciales de modo de enfatizar las teorías de Henkin y para eliminar el problema de las variables compartidas. También definimos nuevas' reglas para la manipulación de los nuevos términos del lenguaje. La semántica denotacional del cálculo es presentada, así como también la demostración de la propiedad Church-Rosser (CR). Además probamos que las reglas de reducción son correctas y que la función semántica está bien definida.