ENIGMA SOBRE C . Terminación de programas

[Serapis]

Hola NEBIREEsta propuesta no vale. Estás describiendo un caso muy partícular de bucles "for", los que se parecen /ajustan al patrón de Pascal

Míralo como quieras, el caso es que el compilador al final tiene que reducir cualesquiera sean las expresiones que contiene cada parte a una única salida, sea un valor constante o variable, al final tiene que ser una gramática no ambigua, sino tendría diferentes interpretaciones y desde hace décadas, se conocen algoritmos para descubrir ambigüedades en las gramáticas.

Así puedes encontrar descrito el bucle for en estos o parecidos términos (he omitido las producciones de otras sentencias de iteración que no vienen al caso):
ejemplo 1:
    stmt = for '(' [ assg ] ';' [ expr ] ';' [ assg ] ')' stmt ';'
https://www2.cs.arizona.edu/~debray/Teaching/CSc453/DOCS/cminusminusspec.html

el metasímbolo '[lo que sea]' expresa que es omitible.

ejemplo 2:
    <iteration-statement> ::= for ( {<expression>}? ; {<expression>}? ; {<expression>}? ) <statement> ;
https://cs.wmich.edu/~gupta/teaching/cs4850/sumII06/The%20syntax%20of%20C%20in%20Backus-Naur%20form.htm

el metasímbolo: '?' denota 0, 1 o más repeticiones.

Pero en el caso de C que se da, que variables hay?, cual es el valor inicial y/o final?
En C, el bucle for es tan versátil/expresivo como el while.
EScrito de otro modo, en el primer caso hay que explicar por qué el bucle C, acaba:

...para eso existe la especificación de un lenguaje.
Todo lenguaje está descrito en determinados términos, hasta hace poco más de una década la notación BNF (BNF-E), se ha demostrado muy práctica, y más recientemente han salido otros modelos que son simples modificaciones del mismo.
Las especificaciones en prosa ( https://frama-c.com/download/acsl_1.2.pdf (la sección 2.4.2 resulta muy ilustrativa), aunque igualmente muy útiles, rara vez resultan tan claras como las dadas formalmente. Lo usual es que se den ambas al mismo tiempo, la prosa explica los detalles que se dan formalmente.
Así todo lenguaje de programación consta de producciones de hecho cualquier lenguaje de programación se considera una gramática libre de contexto, y se suele resumir en una tupla de 4 elementos...
L = {P, T, R, S)
Donde 'P' son todos los símbolos no terminales, variables o producciones de la gramática.
'T', son los símbolos terminales, tokens, componentes léxicos de la gramática.
'R' son las reglas de producciones, la expresión de todas las producciones.
y 'S' es el símbolo inicial, al que resume todo el lenguaje, esto es que representa: 'pertenece al lenguaje', 'es válido para este lenguaje'...

Se habla de producciones, donde cada producción no es ni más ni menos que la equivalencia resumida (como las dos línea arriba expuestas (son parciales)), a la que luego el analizador sintáctico tendrá que recurrir para determinar si es correcto y se ajusta a la descripción o no. No puede haber ambigüedades, así que tu suposición "hay que explicar por qué el bucle C, acaba", está fuera de toda necesidad de suposición. Aunque los componentes sean omitibles, y el analizador sintáctico lo de por válido luego falta el análisis semántico, que será quien se encargue de revisar lo que no puede ser fijado en reglas o resultan excesivamente complejas o previamente no se dispone de toda la info para determinar sus valores. ...y al caso concreto, un compilador debiera prever el caso de un bucle infinito en situaciones sencillas (esas lo son), o si no está adecuadamente programado, caer en dicho bucle infinito y no llegar a finalizar el análisis sintáctico (caso de derivaciones por la derecha). Lo cual siempre dependerá de la implmenetación de cada compilador en específico, y de la incorrecta interpretación de la especificación del lenguaje o en su defecto de un posible error en la propia especificación.

Ojo: No digo que tu razonamiento falle por lado alguno, tan solo digo, que resulta mucho más simple de entender si se recurre a la especificación del lenguaje. En analizador semántico, (si el sintáctico no está mal programado), debe rellenar tales datos antes o después, de tal modo que cuando le toque analizarlo (al semántico), pueda discernir si es o no un bucle infinito, y la regla se resume en la descripción que dí más arriba. Uno puede darle todas las vueltas que quiera, pero el compilador da solo las necesarias.

[Loretz]

El resultado es que cuando 0!=0 entonces ocurrirá que 0 < 0. No dice que 0!=0, sino que cuando 0!=0, absurdo, entonces 0<0 (otro absurdo). Genial!  Pura lógica.

Una proposición falsa implica a todas las proposiciones, verdaderas o falsas. Que uno se encuentre con una aparente consistencia puede favorecer el entusiasmo pero no aporta prueba de nada; lamentablemente la pura lógica no se conmueve con expresiones emocionales

Pero bueno, este es tu acertijo y tus reglas. Por mí está bien, como digas.

[dijsktra]

Una proposición falsa implica a todas las proposiciones, verdaderas o falsas. Que uno se encuentre con una aparente consistencia puede favorecer el entusiasmo pero no aporta prueba de nada; lamentablemente la pura lógica no se conmueve con expresiones emocionales

Pero bueno, este es tu acertijo y tus reglas. Por mí está bien, como digas.

Ejem, ejem.... Veo que has entendido parcialmente el razonamiento: de premisas falsas se llega conclusiones falsas. Es decir, el enigma podría decir que después de acabar el bucle infinito se podía llegar a cualquier cosa: que 2=2, 23=11+25, que la raíz de dos es un número racional.... Tanto verdaderas como falsas... En latín

EX IMPOSSIBILE QUOD LIBET SEQUITUR
(DE LO IMPOSIBLE SE SIGUE CUALQUIER COSA)

Pero no es de recibo desacreditar mi razonamiento por la "sorpresa", o "entusiasmo" en aras a la rigurosidad implacable de la lógica... El razonamiento es absolutamente válido y correcto. Lo que no sería es decir que se concluye que 1==0.

En ningún caso se ha probado que 1=0. Fíjate bien: En el enunciado el autor marcó on terminating the program, realzando al terminar el programa.... Cosa que no ocurre nunca, y por tanto, solo ocurre "en el infinito", lo que puede dar lugar a una contradicción, según el estándar C: 1=0. A partir de ahí, como tú dices, se puede sacar lo que quieras, en particular que assert(1) fallara.

Creo que es compatible con mostrar una reacción de asombro ante  un razonamiento riguroso y objetivo. Sin "smileys" se encuentra la prueba entre etiquetas geshi...

De todas formas, gracias loretz por tu comentario.