blob: e5029b4df9951d55c4ccc637387b16954dc0adfb (
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 = "Evaluability inside of a current context"
date = "2023-02-14"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3f6"]
forwardlinks = []
zettelid = "3c3f6a"
+++
The main important property is also not that one can always find an
execution of a predicate in any context, but that in the current context
that we are proving things in, that one can evaluate it only there. This
is a much easier property to maintain (and is maintained automatically
by the proof), because the semantic interpretation of the forest ensures
that one evaluates all the predicates to some boolean already. This
means that given the current context which can interpret the forest, we
can also interpret any predicate that is inside the forest already.
This also means that if we want to add a new predicate to the forest,
that we need to show we can evaluate it, where the lazy predicate
evaluation is important again.
|
