Theory Phi_BI.Phi_BI
chapter ‹A Bunched Implications Equipped with Satisfaction›
text ‹It also contains a simplified BI specialized for only necessary constructs required
by ∗‹Multi-Term Form›.
➧ ∗‹Multi-Term Form› is the canonical form in the reasoning of φ-System, which demonstrates
abstractions directly and clearly in a localized way. It is characterized by form,
\[ ‹∃a. (x⇩1 ⦂ T⇩1 ∗ x⇩2 ⦂ T⇩2 ∗ ⋯ x⇩n ⦂ T⇩n) ∧ P› \]
where ‹P› is a pure proposition only containing free variables occurring in ‹x⇩1,⋯,x⇩n,a›.
It relates the concrete resource to a set of abstract objects ‹{(x⇩1,⋯,x⇩n) |a. P}› if
∗‹variables ‹a› are not free in ‹T⇩1,⋯,T⇩n››.
All specifications in φ-System are in Multi-Term Form. It is so pervasive that we use a set-like
notation to denote them,
\[ ‹(x⇩1 ⦂ T⇩1 ∗ x⇩2 ⦂ T⇩2 ∗ ⋯ x⇩n ⦂ T⇩n 𝗌𝗎𝖻𝗃 a. P)› \]
Readers may read it as a set,
\[ ‹{ x⇩1 ⦂ T⇩1 ∗ x⇩2 ⦂ T⇩2 ∗ ⋯ x⇩n ⦂ T⇩n |a. P }› \]
➧ ∗‹Simple Multi-Term Form› is a MTF where there is no existential quantification and the attached
‹P› is trivial ‹True›, viz., it is characterized by
\[ ‹x⇩1 ⦂ T⇩1 ∗ ⋯ ∗ x⇩n ⦂ T⇩n› \]
›
text ‹
Specifically, in this minimal specialized BI:
▪ It does not have a general additive conjunction (‹∧›) that connects any BI assertions,
but only the one (‹A 𝗌𝗎𝖻𝗃 P›) connects a BI assertion ‹A› and a pure assertion ‹P›,
because it is exactly what at most the MTF requires.
▪ Implication does not occur in assertions (of φ-SL), but it represents transformations of
abstraction so has a significant role in reasoning (rules).
We emphasize this transformation by assigning the implication with notation
‹A 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 B 𝗐𝗂𝗍𝗁 P ≜ A ⟶ B ∧ P›, where ‹P› is a pure assertion.
The ‹P› helps to capture the information (in abstract domain) lost in the
weakening of this implication.
Currying implications like ‹A ⟶ B ⟶ C› are never used in φ-BI.
▪ Optionally we have universal quantification. It can be used to quantify free variables
if for any reason free variables are inadmissible. The universal quantifier is typically
not necessary in φ-BI and φ-SL, where we use free variables directly. However, in some
situation, like when we consider transitions of resource states and we want a transition
relation for each procedure, we need a single universally quantified assertion,
instead of a family of assertions indexed by free variables.
▪ The use of a implication represents a transformation of abstraction.
Therefore, implications are never curried or nested, always in form ‹X ⟶ Y ∧ P›
where ‹X, Y› are MTF and ‹P› is a pure proposition.
We denote them by notation ‹X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 Y 𝗐𝗂𝗍𝗁 P›.
▪ It only has multiplicative conjunctions, specialized additive conjunction described above,
existential quantification, and optionally universal quantification,
which are all the MTF requires,
plus implications that only occur in reasoning rules.
Any other things, should be some specific φ-Types expressing their meaning
specifically and particularly.
›
theory Phi_BI
imports "Phi_Logic_Programming_Reasoner.PLPR" Phi_Preliminary
abbrevs "<:>" = "⦂"
and "<trans>" = "𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌"
and "<transforms>" = "𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌"
and "<with>" = "𝗐𝗂𝗍𝗁"
and "<subj>" = "𝗌𝗎𝖻𝗃"
and "<when>" = "𝗐𝗁𝖾𝗇"
and "<remains>" = "𝗋𝖾𝗆𝖺𝗂𝗇𝗌"
and "<get>" = "𝗀𝖾𝗍"
and "<map>" = "𝗆𝖺𝗉"
and "<by>" = "𝖻𝗒"
and "<from>" = "𝖿𝗋𝗈𝗆"
and "<remaining>" = "𝗋𝖾𝗆𝖺𝗂𝗇𝗂𝗇𝗀"
and "<demanding>" = "𝖽𝖾𝗆𝖺𝗇𝖽𝗂𝗇𝗀"
and "<to>" = "𝗍𝗈"
and "<over>" = "𝗈𝗏𝖾𝗋"
and "<subst>" = "𝗌𝗎𝖻𝗌𝗍"
and "<for>" = "𝖿𝗈𝗋"
and "<TP>" = "𝒯𝒫"
begin
section ‹Judgement›