blob: be2326a9b6bb4e4aad3635ce7a85a8e106cf4531 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
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.
|
