Si tiene dos funciones que implementan un algoritmo de clasificación diferente, ¿es posible inferir por código fuente que ambas tienen las mismas propiedades externas? ¿Significa que ambos tendrán una posible secuencia sin clasificar como entrada y tendrán una secuencia ordenada como salida? ¿De qué manera el código fuente podría determinar estas propiedades externas? ¿Y cómo describirías estas propiedades externas? ¿Qué notación se usaría?
Las propiedades externas podrían darse a conocer definiéndolas explícitamente, por ejemplo dentro de un sistema de tipos, pero me pregunto si esto podría hacerse implícitamente. ¿O es de alguna manera teóricamente imposible inferir este tipo de semántica? Estoy interesado en saber si esto es posible para funciones arbitrarias, no solo para ordenar algoritmos, asumiendo que cosas como las funciones siempre se detendrán y no tendrán efectos secundarios.
¿Debo mirar la semántica denotacional o no está relacionada?
Me interesan los indicadores para investigar en esta área y los diferentes términos utilizados para describir el tema que podrían ayudar a mi búsqueda de literatura.
fuente
La igualdad de extensión en los lenguajes de programación completos de Turing es indecidible en general, pero eso no debería impedir que pueda verificar o falsificar que dos funciones específicas son extensivamente iguales.
La verificación puede proceder de muchas formas, por ejemplo, podría razonar en la teoría de conjuntos ZFC utilizando la semántica operativa. Sin embargo, eso sería doloroso. Si existe una semántica denotacional, también podrían usarse, pero la buena semántica denotacional solo existe para algunos idiomas. Por lo general, se utilizan lógicas de programa, por ejemplo, lógica de Hoare , para mostrar la igualdad extensional de los programas. Para poder hacer esto, las lógicas de Hoare para idiomas con funciones generalmente requieren un axioma que indique que , suponiendo que y son funciones de tipo (detalles de la variedad del axioma con los detalles del enfoque elegido para la lógica de Hoare).f g α → βF= g⇔ ∀ xα. F( x ) = g( x ) F sol α → β
fuente
Una respuesta rápida (admito que no pasé mucho tiempo ...) El teorema de Rice dice que para cualquier pregunta no trivial, es indecidible decir si la función calculada por un programa tendrá la propiedad o no. Por lo tanto, la pregunta aquí es indecidible
fuente