diff options
Diffstat (limited to 'content/zettel/3c3g4.md')
| -rw-r--r-- | content/zettel/3c3g4.md | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/content/zettel/3c3g4.md b/content/zettel/3c3g4.md new file mode 100644 index 0000000..be2326a --- /dev/null +++ b/content/zettel/3c3g4.md @@ -0,0 +1,23 @@ ++++ +title = "Appending predicated expressions to existing expressions" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3c3g3"] +forwardlinks = ["3c3g5"] +zettelid = "3c3g4" ++++ + +In addition to that, another primitive that is needed is the following +append operation, which will negate the combination of all predicates in +the second predicated type, and it to the first predicated type and +append the first predicated type to the second: + +$$ \mu(p, P) \equiv \texttt{map } (\lambda (p', e') . (p \land p', e'))\ P $$ + +$$ P_{1} \oplus_{p} P_{2} \equiv \mu(\neg p, P_{1}) \mathbin{++} \mu(p, P_{2})$$ + +The append operation, denoted by $\oplus$, will take two predicated +expressions $P_1$ and $P_2$ and negates all the predicates in the second +and anding them to the predicates in the first, while then appending the +whole expression to the previous one. |