The Coq mailing list

[Jan Bessai <jan.bessai AT tu-dortmund.de>]

Would weakly normalizing lambda terms be good enough for your task? If so:

let
  omega := lambda x. x x (terminating)
  Omega := omega omega (non temerminating)
  K := lambda x y. x
in
  K omega Omega (ignores Omega, terminating)

This is fine (and even typeable with intersection types) but cannot be
expressed in Coq.




On 12/19/18 2:40 PM, Siddharth Bhat wrote:
> Is it not possible to provide conductive semantics to such an
> interpreter, and thereby get coq to accept an interpreter? 
> 
> Thanks,
> Siddharth
> 
> On Wed, 19 Dec, 2018, 18:45 Klaus Ostermann,
> <klaus.ostermann AT uni-tuebingen.de
> <mailto:klaus.ostermann AT uni-tuebingen.de>>
>  wrote:
> 
>     I assume an interpreter of Coq in Coq would be such a function.
> 
>     Klaus
> 
> 
>     Am 19.12.18 um 13:53 schrieb Vincent Siles:
>     > Hi !
>     > Today I've been asked if there are some examples of known terminating
>     > programs that can't be expressed at all in Coq. I know the usual
>     > 'fuel' encoding where one can add an integer to recurse on, and then
>     > prove that there always exists an integer big enough for the program
>     > to terminante. But are there examples that are not accepted by Coq
>     > even with such technics ?
>     >
>     > Best,
>     > V.
> 
> -- 
> Sending this from my phone, please excuse any typos!