[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] function signature syntax
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
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.
P.S. Is Dave Stringer Calvert out there somewhere? If so jim says "hiya"!