¿Qué es la realizabilidad?

Answer 1

La semántica de realización es una interpretación de la lógica intuicionista construida a partir de un modelo de computación. Específicamente, expresaré lo siguiente en términos del caso simple de la computabilidad ordinaria, sin embargo, desea tomar eso para que se formalice exactamente.

En la semántica de realizabilidad, consideramos que el valor de verdad de cualquier declaración es un conjunto de cadenas de bits (o lo que sea que consideres que son las entradas / salidas básicas de la computación), la idea es que estas cadenas de bits son los testigos de (también conocidos como “realizadores” de) la verdad de esa declaración. Se considera que una declaración se mantiene solo en caso de que tenga al menos un realizador.

También hay reglas que determinan composicionalmente el valor de verdad de una declaración compleja de las de sus partes constituyentes. Por ejemplo:

• Los realizadores para A y B son los pares ordenados cuyo primer componente es un realizador para A y cuyo segundo componente es un realizador para B
• Los realizadores para A v B son la unión etiquetada de los realizadores para A y los realizadores para B
• Los realizadores para A -> B son aquellas cadenas de bits que, cuando se interpretan como programas de computadora y se proporcionan como entrada a cualquier realizador para A, siempre se detienen y generan algún realizador para B

Uno puede ir más allá y dar cuenta de los cuantificadores de la lógica de primer orden, e incluso pasar a la lógica de predicción de orden superior, donde se habla de “propósitos de realizabilidad” o, en el contexto específico de computabilidad ordinaria, ” topos efectivos “. Sin embargo, una cuenta más completa de estos temas dejaré para más adelante.