The Coq mailing list

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

There is also R as defined by Giannini and Ronchi Della Rocca in [1],
which is strongly normalizing, but does not have a type in System F:

let
  I := lambda x . x
  K := lambda x y . x
  omega := lambda x . x x
in
  (lambda x y . y (x I) (x K)) omega

I cannot see why the proof in [1] would not hold for Coq, but you'd of
course have to verify it.


[1]: Giannini, Paola, and Simona Ronchi Della Rocca. "Characterization
of typings in polymorphic type discipline." Proceedings Third Annual
Symposium on Logic in Computer Science. IEEE, 1988.

On 12/19/18 3:14 PM, Jan Bessai wrote:
> 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!