Another idea for simplifying the proofs

[lordxist]

Goal: Identify the ("intuitively") defining properties of an extraction function, determinism preservation and bisimulation should fall out of those as corollaries.

Basic intuition:

There are two parts that comprise an extraction function:

• an invertible function $f$ specifiying WHAT to extract, and
• a function that returns an equivalent copattern and specifies HOW to extract

The latter function is already present as $\langle \cdot \rangle^{\sim}$ in the preliminary 3rd thesis chapter.

Common definition for the extraction functions:

Using these two functions, the general form of an extraction function $e$ can be specified as follows:

• $e$ extracts out of all equations with lhs of the form $f^{-1}(q)$ for some copattern $q$
• $e$ leaves all other equations unchanged
• for equations $r$ where an actual extraction takes place, the result of the extraction are two equations $\epsilon_r, \zeta_r$ defined as follows:
  • $q_{\epsilon_r} = \langle q_r \rangle^f$
  • $t_{\epsilon_r} = \langle \langle q_r \rangle^f \rangle^{\sim}$
  • $q_{\zeta_r} = \langle \langle \langle q_r \rangle^f \rangle^{\sim} \rangle^{f^{-1}}$
  • $t_{\zeta_r} = t_r$

    Applied to the concrete extractions:

extract_des: f removes a destructor: $f(``q'_r.des(\overline{p})") = q'_r$ the equivalent copattern that specifies how to extract: $\langle q \rangle^{\sim} = \langle q \rangle^{hname}(\langle q \rangle^{vars})$

extract_con: f removes a constructor: $f(fun(p, \overline{p}, con(\overline{p'}), \overline{x})") =fun(\overline{p}, \langle con(\overline{p'}) \rangle^{f_p}, \overline{x})"$ with $f_p(con(\overline{p}, con(\overline{p'}), \overline{x})") =con(\overline{p}, \langle con(\overline{p'}) \rangle^{f_p}, \overline{x})"$, $f_p(``con(\overline{x})") = y$ the equivalent copattern that specifies how to extract: $\langle q \rangle^{sim} = \langle q \rangle^{hname}(...)$

[lordxist]

A further refinement of the $f$ function part of the extraction function:

For every copattern $q$, there is a substitution or co-substitution (see below) $\sigma^q_f$ such that: $\sigma^q_f(\langle q \rangle^f) = q$

Co-substitutions

A function $\sigma$ from copatterns to copatterns is called a co-substitution, if, for every copattern $q$, it is defined as follows: $\sigma(q) = q.\overline{des(\overline{p})}$, for some $\overline{des(\overline{p})}$ possibly depending on the $q$.

[lordxist]

Lenses

Instead of with $f$ and $f^{-1}$, the situation above is better expressed with lenses, where $f$ takes the part of get. And using the substitution/co-substitution $\sigma^q_f$ from the previous comment, the lens can be expressed as follows, where $q^c$ is the copattern out of which is extracted, and $q^a$ is any copattern.

$get(q^c) = \langle q^c \rangle^f$ $putback(q^a, q^c) = \sigma^{q^c}_f(q^a)$