[PVS-Help] function signature syntax

["jim armstrong" <armstrong.jm@xxxxxxxxx>]

I am currently baffled by the syntax for function signatures used on Page 18 of the PVS Language Reference.

It probably  boils down to fact that I do not understand how to parse typed lambda calculus, but anyway.

On P.18 we are shown the shorthand definition:

x, y, w : VAR int

z : VAR nat

f(x) (y, z) (w):int = x * (y + w) - z


PVS typechecks all this without TCCs. 

But I cannot parse the lhs of this equation. In particular the argument pairing (y, z) baffles me. 

The precedence here is: (x * (y+w)) - z

The subtraction is outermost. So I read the expression on the rhs as having type [INT, NAT -> INT] - or when expanded into the rather odd form of lambda calculus:   [INT -> [INT, INT -> [NAT -> INT]]]

But the text on p.18 has   [INT -> [INT, NAT -> [INT -> INT]]].

Note the position of the NAT type.

Even more puzzling to me, is that when I typecheck the following:

f2(x) (y, w)  (z):int = x * (y + w) - z

I get the following TCC:

 Subtype TCC generated (at line 36, column 11) for  w
    % expected type  nat
  % unfinished
precedencef2_TCC1: OBLIGATION FORALL (w: int): w >= 0;

This is looks to be unprovable since w is an int - but why it is generated at all I can't imagine.

Any help or advice appreciated.

regards

jim armstrong

P.S. Is Dave Stringer Calvert out there somewhere? If so jim says "hiya"!