No existe una respuesta única a esta pregunta, debido al alto grado de no determinismo inherente al cálculo secuencial: para obtener una interpretación computacional, es necesario resolver la ambigüedad, y cada forma de hacerlo conduce a diferentes interpretaciones operativas. Además, las respuestas difieren en cierta medida para los cálculos secuenciales clásico e intuicionista.
Las asignaciones de términos de prueba para los cálculos secuenciales clásicos se corresponden estrechamente con los cálculos de continuación, como el de Herbelin $\lambda\mu$ cálculo. Ahora bien, las transformaciones de continuación corresponden a traslaciones de doble negación de la lógica clásica a la lógica intuicionista, y hay muchas traslaciones de doble negación posibles. Cada elección de traducción de doble negación da lugar a un orden de evaluación diferente, lo que explica por qué son tan valiosas para el estudio de las máquinas abstractas (como en el enlace de supercooldave) - se pueden obtener los beneficios de estudiar diferentes órdenes de evaluación a través de las transformaciones CPS, sin tener que codificar todo en funciones.
Ahora bien, también se puede intentar eliminar el no determinismo de otra manera: por decreto. Esto se basa en la idea de Andreoli de enfoque para la lógica lineal. En términos operativos, la idea es definir las conectivas lógicas en términos de sus valores o de sus formas de eliminación (esto se denomina polaridad ). Después de elegir uno, el otro viene determinado por la necesidad de satisfacer la eliminación de cortes. Para la lógica lineal, cada una de las conectivas tiene una polaridad única. Para la lógica clásica, cada conectiva puede tener una u otra polaridad (es decir, cada conectiva puede definirse en términos de valores o de continuaciones), y la elección de las polaridades de las conectivas determina esencialmente el orden de evaluación. Esto se explica muy bien en la tesis doctoral de Noam Zeilberger, http://www.cs.cmu.edu/~noam/tesis.pdf .
En el caso de los cálculos secuenciales intuicionistas, las asignaciones de términos de prueba aún contienen mucho no determinismo. Cuando se resuelve esto mediante la focalización, se encuentra que los cálculos resultantes son cálculos de concordancia de patrones . En la tesis de Noam también hay una hermosa versión abstracta de este tema, y yo escribí un artículo muy concreto al respecto para POPL 2009, "Centrarse en la concordancia de patrones" que mostraba cómo explicar la concordancia de patrones al estilo Haskell/ML en términos de asignación de términos de prueba para cálculos secuenciales focalizados.
