blob: 167092b6ecc826aeb012af26c78624a97d40d2c3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
+++
title = "Predicate with integer evaluation"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["2e1b3c2", "2e1b3c"]
forwardlinks = ["2e1b3b", "2e1b3c2"]
zettelid = "2e1b3c1"
+++
The first possibility is to extend the notion of predicates with two
arguments ([\#2e1b3b]), to having multiple arguments. This can be done
by having a predicate that evaluates to a natural number, which is then
used to select the right variable.
However, this has multiple downsides, one being that the predicate
basically becomes a function that is opaque to the outside definitions.
It would therefore have to carry around many proofs about properties
that need to hold for the function, such as it being injective and
getting the right property.
It being a function would also make it difficult to analyse from the
outside, and it would then also be difficult to do symbolic analysis on
the predicates. Having a syntactic representation of this kind of
function would also be quite complex, and would come with it's own
problems. The predicate would have to be quite complex, reducing the
amount of analysis that one can do.
[\#2e1b3b]: /zettel/2e1b3b
|
