blob: bc08fd743951f0bb0bb24b8d3cfa7ed909cf3fca (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
+++
title = "Combining linear predicated expressions"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3g2"]
forwardlinks = ["3c3g4"]
zettelid = "3c3g3"
+++
$$ P_{1} \otimes P_{2} \equiv \texttt{map } (\lambda ((p_{1}, e_{1}), (p_{2},e_{2})) . (p_{1} \land p_{2}, f\ e_{1}\ e_{2}))\ P_{1} \times P_{2} $$
The expressions are then constructed using a function which updates the
symbolic expressions assigned for each resource. This is done using
multiple primitives which act on predicated types, which are made up of
a list of pairs of predicates and the element of that type. The first
important primitive is multiplication of two predicated types, which is
implemented as performing a cartesian multiplication between the
predicated types in the two lists, anding the two predicates and joining
the two types of each list using a function.
|
