Simon-Kor
commented
2 months ago Problem with produced Assumption,
Right now the Assumption that would be added is not correct, the parenthesis are incorrect. Also the domain check for well defines could easily be done wrong. Therefore the local definition should be corrected to.
The real problem is the bounding of free variables in the expression and subdomain definition. Since in the expression we could use global constants and free variables, which are indirect bounded by our subdomain but this has to be done realy carefully so we don't have any logical mistake there.
Since we are dealing with the argument variable, global constants(free variables) and locally bounded we could introduce following steps to be sure that our function is well defined.
First we do for every case of a local function definition a optional grammar rule where all locally bounded variables which are in the expression are stated explicitly, and we do a check such that all variables contained in the expression is either constant, the argument variable or will be universially bounded.
Then since we bound the local variables universiably, we need to be really precies to have a well defined function. Therefore we have to set the proof goals for a local function to a XOR of all subdomain statments. As a generic example.
Let $f: \reals \to \naturals$ such that $f(x) =$
\begin{cases}
&0 &\text{if} x < 0 \\
&k &\text{if} x \in \[k, k+1\) \text{where} k \in \naturals
\end{cases}
Let $f: X \to Y$ such that $f(x) =$
\begin{cases}
& \eta_1(x,v_{1,1}, ... ,v_{n,1}) &\text{if} \phi_1(x,v_{1,1}, ... , v_{n,1}) \text{where} v_{1,1} \in D_{1,1}, ... , v_{n,1} \in D_{n,1}
...
& \eta_m(x,v_{1,m}, ... ,v_{n,m}) &\text{if} \phi_1(x,v_{1,m}, ... , v_{n,m}) \text{where} v_{1,m} \in D_{1,m}, ... , v_{n,m} \in D_{n,m}
\end{cases}The second case should be result in this assumptions and proof goals.
We let \eta denote a expression and \phi is a formula.
Assumptions:
\forall x,v_1, ... v_n . [ ( \phi_1(x,v_1, ..., v_n) \land x \in X \land (..., v_i \in D_i , ... ) ) => ( f(x) = \eta_1(x,v_1, ... , v_n) ) ]
...
\forall x,v_1, ... v_n . [ ( \phi_m(x,v_1, ..., v_n) \land x \in X \land (..., v_i \in D_i , ... ) ) => ( f(x) = \eta_m(x,v_1, ... , v_n) ) ]Proof Goals(well definiteness): First for all x \in X we have only one \phi_i which is true so: Goal 0 :=
\forall x, v_{1,1}, ... , v_{n,1}, v_{1,2}, ... v_{n,m-1} , v_{1,m}, ... ,v_{n,m} . [
x \in X,
v_{1,1} \in D_{1,1}, ... , v_{n,1} \in D_{n,1}, ..., ..., v_{n,m} \in D_{n,m}
=>
XOR_{i \in \{1, ... , m\} } \phi_i (..) ] exactly one Then we check for all cases, where such locally bounded variables (vs) are in the expression and let the index set of these be
J = \{ j \in \{1, ..., n\} \mid (\text{free variables}(\phi_j) \setminus \{x\}) \neq \emptyset \}. Goal $j$ with $j \in J$ :=
\forall x \in X ,
\forall v_{1,j}, ... v_{n,j}, v'_{1,j}, ..., v'_{n,j} [
(v_{1,j}, v'_{1,j} \in D_{1,j}), ..., (v_{n,j}, v'_{n,j} \in D_{n,j})
if \phi_j (x, v_{1,j}, ... v_{n,j}) \land \phi_j (x, v'_{1,j}, ... v'_{n,j})
then \eta_j (x, v_{1,j}, ... v_{n,j}) = \eta_j (x, v'_{1,j}, ... v'_{n,j}) ]The last goal could be substituted with a goal that exacly one combinations of vs could be true for every x.
This looks very difficult to be proven by the ATP, but since in the real case of usage this vs would only be a handful not as many as be the general case would indicate.
The local function definition is now implemented, but there are some problems, which need a further improvements.
The local definition is right now consistent in terms of the corresponding domain and the subdomains. The range off this function is right now black boxed and could easily result in inconsistency, since we add the assumption that for all x in the domain we have f(x) is in the range.
After all we only check right now that for all x we have x is in the domain if and only if x fulfills exactly one statement of the subdomains. This don't support a good checking of a vaild statment, there should be a validation if the current state is right or that there is a need of a better check.