(**************************************************************************) (* *) (* Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, *) (* Kim Nguyen, Laurent Sartre *) (* *) (* Informatique - MP2I/MPI - CPGE 1re et 2e années. *) (* Cours et exercices corrigés. Éditions Ellipses, 2022. *) (* *) (* https://www.informatique-mpi.fr/ *) (* *) (**************************************************************************) (* Preuve du théorème de Rice : un générateur de solutions au problème de l'arrêt. *) let c (s1: string) (s2: string) (f: string -> bool): string -> string -> bool = let halts (s: string) (e: string): bool = f ("let _ = try eval s e with _ -> s in " ^ s2) <> f s1 in halts