Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus