Prouver la terminaison à la main

Prouver la terminaison à la main. On considère quatre fonctions.

def f(n):          # n entier positif ou nul
    while n > 0:
        n = n - 2

def g(a, b):       # a et b entiers, au moins 1
    while a != b:
        if a > b:
            a = a - b
        else:
            b = b - a
    return a

def h(n):          # n entier, au moins 1
    while n != 1:
        if n % 2 == 0:
            n = n // 2
        else:
            n = 3 * n + 1

def k(n):          # n entier quelconque
    while n != 0:
        n = n - 2

• Montrer que f et g s'arrêtent toujours, en exhibant pour chacune un variant : une quantité entière, positive tant que la boucle tourne, qui diminue strictement à chaque tour.
• Donner une valeur de n pour laquelle k ne s'arrête pas. Pour quelles valeurs s'arrête-t-elle ?
• La fonction h suit la suite de Syracuse. Que sait-on de sa terminaison ?
• Pourquoi ne peut-on pas confier ce travail à un programme qui répondrait pour toutes les fonctions ?