Implement and termination metrics

[Yannick Duchêne]

I never noticed before, it seems termination metrics cannot be used with separate declaration and implementation. Or am I missing something?

Additionally, I noticed declaring a function to have no effects, does not require its implementation to have termination metrics unlike what it is when a function is declared and implemented in the while.

With declaration and implementation in the while:

        // Postiats complains termination metrics is missing.

        fun f {i:int | i >= 0} (i:int(i)):<> void =

          if i > 0 then f(i - 1)

          else ()

        // With terminations metrics added, there is no error.

        fun f {i:int | i >= 0} .<i>. (i:int(i)):<> void =

          if i > 0 then f(i - 1)

          else ()

With separate declaration and implementation:

        extern fun f {i:int | i >= 0} (i:int(i)):<> void

        // No termination metrics and Postiats does not complain.

        implement f {i:int} (i:int(i)): void =

          if i > 0 then f(i - 1)

          else ()

Anyway, if it’s not possible to add termination metrics with `implement`, if Postiats was complaining, it could not be solved.

After that, may be it’s better to not use separate declaration and implementation with functions ; well, at least if ensuring all functions are terminating is important.

[gmhwxi]

Yes, this is a "loophole".

Strictly speaking, 'implement' should only be used to

implement non-recursive functions. But this is too big

a restriction in practice.

[Yannick Duchêne]

Le jeudi 2 août 2018 06:39:05 UTC+2, gmhwxi a écrit :

[…]

Strictly speaking, 'implement' should only be used to

implement non-recursive functions. […]

That’s an interesting reply, some more thing I will need to meditate about …