From: Ferruccio Guidi Date: Fri, 24 Dec 2021 09:50:41 +0000 (+0100) Subject: update in delayed updating X-Git-Tag: make_still_working~122 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9605ffc88831066a901ea4eb8e419f277662f372;p=helm.git update in delayed updating + delayed focalized reduction --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/circled_times_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/circled_times_1.ma new file mode 100644 index 000000000..ac8c482a9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/circled_times_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( ⊗ term 60 p )" + non associative with precedence 60 + for @{ 'CircledTimes $p }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/pitchfork_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/pitchfork_2.ma new file mode 100644 index 000000000..1cfe14b61 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/pitchfork_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( t ⋔ break p )" + left associative with precedence 47 + for @{ 'Pitchfork $t $p }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/pitchforkleftarrow_3.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/pitchforkleftarrow_3.ma new file mode 100644 index 000000000..7ab607d39 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/pitchforkleftarrow_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( t [ ⋔ break term 46 p ← break term 46 u ] )" + non associative with precedence 47 + for @{ 'PitchforkLeftArrow $t $p $u }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_squarecap_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_squarecap_1.ma new file mode 100644 index 000000000..dbe1a242d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_squarecap_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( ⊓ term 46 p )" + non associative with precedence 45 + for @{ 'PredicateSquareCap $p }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma new file mode 100644 index 000000000..f0b3f5f31 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/xoa/ex_3_1.ma". +include "delayed_updating/syntax/path_structure.ma". +include "delayed_updating/syntax/path_balanced.ma". +include "delayed_updating/substitution/fsubst.ma". +(* +include "delayed_updating/notation/functions/pitchforkleftarrow_3.ma". +*) + +(* DELAYED FOCALIZED REDUCTION **********************************************) + +inductive dfr (p) (q) (t): predicate preterm ≝ +| dfr_beta (b) (n): + let r ≝ p;;(𝗔;b;;(𝗟;q,𝗱❨n❩)) in + r ϵ t → ⊓⊗b → dfr p q t (t[⋔r←t⋔p,𝗦]) +. +(* +interpretation + "focalized substitution (preterm)" + 'PitchforkLeftArrow t p u = (fsubst p u t). +*) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma new file mode 100644 index 000000000..0ff05222b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/xoa/ex_3_1.ma". +include "delayed_updating/syntax/preterm.ma". +include "delayed_updating/notation/functions/pitchforkleftarrow_3.ma". + +(* FOCALIZED SUBSTITUTION ***************************************************) + +definition fsubst (p) (u): preterm → preterm ≝ + λt,q. + ∨∨ ∃∃r. r ϵ u & p ϵ ▵t & p;;r = q + | ∧∧ q ϵ t & (∀r. p;;r = q → ⊥) +. + +interpretation + "focalized substitution (preterm)" + 'PitchforkLeftArrow t p u = (fsubst p u t). diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/path_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/path_dephi.ma new file mode 100644 index 000000000..f51295ecf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/path_dephi.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/relocation/tr_pap.ma". +include "delayed_updating/syntax/path.ma". + +(* DEPHI FOR PATH ***********************************************************) + +rec definition path_dephi (f) (p) on p ≝ +match p with +[ list_empty ⇒ 𝐞 +| list_lcons l q ⇒ + match l with + [ label_node_d n ⇒ 𝗱❨f@❨n❩❩;path_dephi f q + | label_edge_L ⇒ 𝗟;path_dephi (𝟏⨮f) q + | label_edge_A ⇒ 𝗔;path_dephi f q + | label_edge_S ⇒ 𝗦;path_dephi f q + ] +]. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/preterm_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/preterm_dephi.ma new file mode 100644 index 000000000..60c5a4a41 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/preterm_dephi.ma @@ -0,0 +1,21 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "delayed_updating/syntax/path_dephi.ma". +include "delayed_updating/syntax/preterm_constructors.ma". + +(* DEPHI FOR PRETERM ********************************************************) + +definition preterm_dephi (f) (t): preterm ≝ + λp. ∃∃q. q ϵ t & p = path_dephi f q. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma new file mode 100644 index 000000000..3226657d4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "delayed_updating/syntax/path.ma". +include "delayed_updating/notation/relations/predicate_squarecap_1.ma". + +(* BALANCE CONDITION FOR PATH ***********************************************) + +(* This condition applies to a structural path *) +inductive pbc: predicate path ≝ +| pbc_empty: pbc 𝐞 +| pbc_redex: ∀b. pbc b → pbc (𝗔;b,𝗟) +| pbc_after: ∀b1,b2. pbc b1 → pbc b2 → pbc (b1;;b2) +. + +interpretation + "balance condition (path)" + 'PredicateSquareCap p = (pbc p). diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_dephi.ma deleted file mode 100644 index f51295ecf..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_dephi.ma +++ /dev/null @@ -1,30 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "ground/relocation/tr_pap.ma". -include "delayed_updating/syntax/path.ma". - -(* DEPHI FOR PATH ***********************************************************) - -rec definition path_dephi (f) (p) on p ≝ -match p with -[ list_empty ⇒ 𝐞 -| list_lcons l q ⇒ - match l with - [ label_node_d n ⇒ 𝗱❨f@❨n❩❩;path_dephi f q - | label_edge_L ⇒ 𝗟;path_dephi (𝟏⨮f) q - | label_edge_A ⇒ 𝗔;path_dephi f q - | label_edge_S ⇒ 𝗦;path_dephi f q - ] -]. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma new file mode 100644 index 000000000..d7608ba18 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "delayed_updating/syntax/path.ma". +include "delayed_updating/notation/functions/circled_times_1.ma". + +(* STRUCTURE FOR PATH *******************************************************) + +rec definition path_structure (p) on p ≝ +match p with +[ list_empty ⇒ 𝐞 +| list_lcons l q ⇒ + match l with + [ label_node_d n ⇒ path_structure q + | label_edge_L ⇒ 𝗟;path_structure q + | label_edge_A ⇒ 𝗔;path_structure q + | label_edge_S ⇒ 𝗦;path_structure q + ] +]. + +interpretation + "structure (path)" + 'CircledTimes p = (path_structure p). diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma index 44d923d9b..aabb5adae 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma @@ -14,6 +14,7 @@ include "ground/lib/subset.ma". include "delayed_updating/syntax/path.ma". +include "delayed_updating/notation/functions/pitchfork_2.ma". include "delayed_updating/notation/functions/uptriangle_1.ma". (* PRETERM ******************************************************************) @@ -21,8 +22,15 @@ include "delayed_updating/notation/functions/uptriangle_1.ma". (* Note: preterms are subsets of complete paths *) definition preterm: Type[0] ≝ 𝒫❨path❩. +definition preterm_grafted: path → preterm → preterm ≝ + λp,t,q. p;;q ϵ t. + +interpretation + "grafted (preterm)" + 'Pitchfork t p = (preterm_grafted p t). + definition preterm_root: preterm → preterm ≝ - λt,p. ∃q. p;;q ϵ t. + λt,q. ∃r. q;;r ϵ t. interpretation "root (preterm)" diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma deleted file mode 100644 index 60c5a4a41..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma +++ /dev/null @@ -1,21 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "delayed_updating/syntax/path_dephi.ma". -include "delayed_updating/syntax/preterm_constructors.ma". - -(* DEPHI FOR PRETERM ********************************************************) - -definition preterm_dephi (f) (t): preterm ≝ - λp. ∃∃q. q ϵ t & p = path_dephi f q.