Predicative semantics of loops