Resumen

En 1994, Matthews introdujo la noción de espacio métrico parcial con el objetivo de proporcionar un modelo matemático cuantitativo adecuado para la verificación de programas. Concretamente, Matthews demostró una versión del teorema del punto fijo de Banach en un espacio métrico parcial, que se ha convertido en una técnica de punto fijo cuantitativa apropiada para capturar el significado de especificaciones denotacionales recursivas en lenguajes de programación. En este artículo mostramos que algunas suposiciones en la declaración del teorema del punto fijo de Matthews pueden relajarse para proporcionar una técnica de punto fijo cuantitativa útil para analizar el significado de las mencionadas especificaciones denotacionales recursivas en lenguajes de programación. En particular, demostramos un nuevo teorema de punto fijo para autoaplicaciones entre espacios métricos parciales en el que la completitud ha sido reemplazada por 0-completitud y la condición contractiva ha sido debilitada de tal manera que la nueva se ajusta mejor a los requis

• Materias:Ecuaciones diferenciales Dinámica de fragmentación Medios porosos Circuito abierto
• Subjects:Differential equations Fragmentation dynamics Porous media Open circuit
• Palabras claves:Introducido; Espacio métrico parcial; Teorema del punto fijo de Banach; Especificaciones denotacionales recursivas; Técnica del punto fijo; Lenguajes de programación
• Keywords:Introduced; Partial metric space; Banach fixed point theorem; Recursive denotational specifications; Fixed point technique; Programming languages