+++
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.