2
$\begingroup$

I was thinking that in the formal model (or symbolic model?) the destructor terms were used to model processes that could abort generating some errors or something like that. But then, I realized that it doesn't make sense because Processes are different structures, they are not terms.

So, I found this slide that defines destructors and constructors terms on the page eight as follows:

  • Constructors are used to build terms

  • Destructors manipulate the terms

But it is still unclear to me. Any function manipulate terms and they may be used to build terms... Thus, are these two sets of terms not disjoint?

Well, could someone explain the difference between these two types of terms and say their right definitions ?

$\endgroup$
1
$\begingroup$

Now I think I know what are constructor terms and destructor terms.

Constructors are used to build terms

means that there is no correspondent term to represent the application of a constructor to others terms. They are function symbols (like $enc$, to represent encryption) that are applied to other terms resulting in another (like $enc(m, k)$ to represent the encryption of $m$ using key $k$. The term $enc(m, k)$ is not in the list of terms $T$, so, it is a built term).

Destructors manipulate the terms

as I thought, this sentence is not clear. In fact destructors are applied to other terms just like constructors, but they are interpreted and substituted by other terms. For instance, $dec$ is a destructor term that represents the decryption algorithm and $dec(enc(m, k), k)$ is reduced to the term $m$.

And finally, what I said about destructors in the question was not too wrong... As stated in page 18 of these MPRI notes: "Destructors are used to model the fact that some operations fail."

So, for instance, $dec(enc(m, k_0), k_1)$ fails if $k_0 \not = k_1$, and the process doing the substitution may block or treat the failure.

For instance, assuming $g$ is a destructor, the process

let $x = g(M_1 , ... , M_n )$ in $P$ else $Q$

bounds $x$ to the resulting of $g(M_1 , ... , M_n )$ and then execute $P$, or, execute $Q$ if $g$ fails.

$\endgroup$
  • $\begingroup$ Please, feel free to discuss this answer and say if something here seems weird to you. $\endgroup$ – Hilder Vitor Lima Pereira Mar 9 '16 at 17:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.