Re: [isabelle] flatten of tuples



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

On 02/27/2015 01:32 PM, Larry Paulson wrote:
> 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 at 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
>
>
>> On 27 Feb 2015, at 02:09, Viorel Preoteasa <viorel.preoteasa at aalto.fi> wrote:
>>
>> 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
>>
>>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.