Email Gateway (Aug 19 2022 at 17:07): Email Gateway (Aug 19 2022 at 17:07):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hello,
Is it possible to have a semantic construct which works like
(a,b,c,d) @ (x,y,z) = (a,b,c,d,x,y,z)
for tuples of arbitrary lengths.
The elements a, b, ... should be of different types,
but they are not tuples.
I can also work with a version which has a terminator like:
(a,b,c,d,()) @ (x,y,z,()) = (a,b,c,d,x,y,z,())
If this is not possible at the semantic level, is it possible
to have a syntactic construct?
Best regards,
Viorel Preoteasa
Email Gateway (Aug 19 2022 at 17:07):From: Larry Paulson <lp15@cam.ac.uk>
An operator such as your @ seems unlikely to exist, because its operands would not have fixed types. What you mean by “syntactic construct” isn’t clear, unless you never need to write a thing like x@y.
I imagine that you cannot use lists because you need a variety of types. But is there is no possibility of creating a super type for them?
Larry Paulson
Email Gateway (Aug 19 2022 at 17:08):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hi Larry,
Thank you for your answer.
I want to model some "product of programs" in the following way:
S is a program with inputs x (tuple) and v (also tuple) and outputs y
(tuple) and u (tuple).
S' is similar but with inputs x', v' and outputs y', u'
I want the result of the product of S and S' to have input (x @ x') and
(v @ v')
and output (y @ y') and (u @ u').
I have a simple product S * S' that has (x,v), (x',v') as input and
(y,u), (y', y') as output.
If I would have the operator @, then I will define my product S ** S' as
[X, V --> (x,v), (x',v') . X = (x @ x') /\ V = (v @ v')] o (S * S') o
[(y,u), (y',u') --> Y,U . Y = (y @ y') /\ U = (u @ u')]
Here [x,y --> a, b . P x y a b] is the nondeterministic assignment of
values to a and b based on
input x, y such that P x y a b is true.
The programs are modeled as predicate transformers, and I can write in
Isabelle
the above composition almost like I have it here, except that I do not
have @.
Ideally the splinting of X and V in the first statement in (x @ x') and
(v @ v')
would be based on the type of S * S'.
These programs are supposed to work with variables of different types
mixed together (real, int, nat, bool). I can create a super type of them
but then the verification of these programs will become more complicated.
Lists are also not good because I could no longer encode in the type the
number
of arguments a program expects as input.
In my case these programs are automatically generated, so in principle
I know the structure of the tuples x, v, x', v' ..., so I can generate
instead
of the general product from above, specialized versions for the specific
x, v, x', v' ...
Best regards,
Viorel Preoteasa
Email Gateway (Aug 19 2022 at 17:08):From: Larry Paulson <lp15@cam.ac.uk>
Personally, I would try to model values in your example using the hereditarily finite sets, as illustrated in my recent AFP paper and entry:
Paper: http://www.cl.cam.ac.uk/~lp15/papers/Formath/automata.pdf
AFP entry:
http://afp.sourceforge.net/entries/Finite_Automata_HF.shtml
Into this one type, you can naturally embed integers, booleans, characters, rationals, along with lists and trees built over them. You can also embed floating-point numbers, but not real numbers. Possibly that would be enough for your purposes. In the development version of the AFP, I’ve installed a file that defines a new type class, finitary, of types equipped with an embedding into HF. This is open-ended, because anything that is essentially a finite construction can be represented by a hereditarily finite set.
Larry Paulson
Email Gateway (Aug 19 2022 at 17:08):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Thank you. I will check your paper.
I used in the past one single type to represent all values from
a program. It was OK, but I could not have the type
checker solve type miss matches anymore. Maybe
using hereditarily finite sets is different.
This was in PVS, using dependent types. The problem
was that dependent types could be only uninterpreted,
or subtypes of a given type.
Viorel Preoteasa
Last updated: Apr 24 2024 at 01:07 UTC