On Friday, November 2, 2012 1:14:26 PM UTC-7, Graham Cooper wrote:
> ALL(X) is a difficult function to define as it's an INTRA FUNCTION, it
> has access to the arbitrary particular string which is how we define
> functions with arbitrary symbols.
That wasn't too helpful to me. What do you mean by "INTRA FUNCTION"?
The best I could find was from http://www.cs.rochester.edu/u/xiaoming/csc254-intra-function-code-gen...
Grammar modification for control flow: (i.e. all intra-function control flow is changed to gotos and if-gotos.) <if-statement> --> if left_parenthesis <operand> <comparison op> <operand> right_parenthesis goto LABEL semicolon
<goto-statement> --> goto LABEL semicolon
<label-statement> --> LABEL colon
LABEL is just another name for ID token
> ALL(X) E(Y) Y = X + 1
> is the same function as
> ALL(A) E(B) B = A + 1
For all A there exists a B where B = A + 1.
OK, you are defining A and B as the free variables
in the expression B = A + 1. I think I understand.
> So if you use P = [X = Y + 1]
Why would you do that? What does P respresent?
> How can you Quantify over P by treating it as a function argument?
> ALL(A) P
> has forgotten what the variable names are inside P and is meaningless!
It would be helpful if you stuck as close as possible to a single
syntax unless you are responding to some one who uses a different
syntax and seems less willing to adjust.
> BORROWING off PROLOG SYNTAX, or HORN CLAUSES
> but we will only examine an atomic predicate.
> PROLOG ATOMS
> # here I use the word predicate for the predicate name, not including
> the arguments.
I'm not sure what you mean by a predicate here. Sure, prolog has
a loose meaning but as far as I know for prolog a predicate is a
term with or without qualificaiton. That is "true" is a built in
predicate as is "false" as is "assert(X)". Heck I've just (re)learned
"!" and "fail" are predicates.
> A term is written in lowercase such as tom, fred, 0, 1, set1, nums,
> A VAR or VARIABLE is written in uppercase.
> Prolog uses the DOUBLE VARIABLE INSTANTIATION RULE.
> Here is a Prolog predicate that returns true iff the X [c]ordinates are
> the same.
> vertical( point(X,Y) , point(X,Z) ).
I'm still relearning prolog just for you.
How do I know when vertical returns
YES, NO, or vertical(point(1,3), point(1,5))?
> FORALL vs FORANY
> Let's examine the AXIOM OF EXTENSIONALITY
> ALL(S1) ALL(S2) ALL(X) (XeS1 <-> XeS2) <-> (S1=S2)
I still don't understand XeS1. I think you mean X is an element of S1.
is that correct or incorrect?
> Procedurally the ALL(S1) ALL(S2) are not required.
> This works equally as well.
> ANY(S1) ANY(S2) ALL(X) (XeS1 <-> XeS2) <-> (S1=S2)
Now I'm confused. You used E(X) above to mean exists, or so
I thought. This seems to imply "ANY" is distinct from "E" (exists).
I don't know of any formal quantifiers other than universal and
existential. In informal language we might say "any one who bites
on that is a fool. We'd typically translate that to:
ALL(X)(bites(X,that) -> fool(X))
Why have you introduce a new quantifier?
> But note:
> ANY(S1) ANY(S2) ANY(X) (XeS1 <-> XeS2) <-> (S1=S2)
> ANY(X) is ambiguous, does the equation hold for ANY X
> or is there any X for which the equation CAN hold?
> meaning the same as EXIST(X)!
Yes, I would agree your use of ANY was ambiguous. More
so, I took it as a variety of existential quantification
until I remembered your use of E(X) above. I like your
use of EXIST(X) as a quantifier better and would prefer
you used ELEMENT_OF(x,S1) as well. I'll use it here:
ESISTS(S1) EXISTS(S2) ALL(X)(
(ELEMENT_OF(X,S1) <-> ELEMENT_OF(X,S2)) <-> (S1=S2))
is a pretty weak claim. It leaves open the possibility
that there exists S1 and S2 for which S1 and S2 contain
exactly the same elements but we wouldn't say the sets
> In PROLOG, S1 and S2 work just by using the double variable
> instantiation rule to match to any (1) value of sets in the current
> model under examination.
Google didn't turn up any definition for "double variable
instantiation rule". I'll have to try to determine it from
context since I don't know what you mean here.
> TOWARDS PROLOG
> ALL(X) (XeS1<->XeS2) <-> (S1=S2)
> The ALL(X) is MANDATORY! It cannot be processed using double
> variable instantiation rule.
I don't get what you are saying but I have a suggestion. I
don't know if it will work.
if it works should return
I don't know. I don't have a prolog compiler
or interpretor and don't remember prolog.
(must later I came back here. found http://www.complang.tuwien.ac.at/ulrich/Prolog-inedit/ISO-Hiord
have you implemented that?
I would have thought you implemented
p(X) to return all X in p. For instance, using the above facts:
> ALL( string ) is a predicate type that returns the conjunction
> of all boolean values of the predicate string argument for all
> solutions of the variable ALL.
More work needed. ALL returns a list of TRUE and FALSE?
> e.g. INDUCTION FORMULA
> p(0) & ALL(n) p(n)->p(s(n))
> -> ALL(n) p(n)
I don't get this at all. If you assert the fact:
Then this function:
X > 0,
Xp is X - 1,
should have the following behavior
I don't know what would be returned by
I'm thinking I've defined a very inefficient
routine where using the mod function would be
> Using HIGH ORDER PROLOG method.
> p(0) ^ N(p(N)->p(s(N))
> -> N(p(N))
What does "HIGH ORDER PROLOG" reference?
Certainly nothing that looks like what you wrote.
> This notation provides a direct computational method for
> backward chaining formula to their axiomatic derivation
> by using double variable instantiation on the ALL type predicate
> inside the predicate and branching into width first (conjunction)
> solution search mode in a modified Unify() algorithm.
More work. More coding in prolog if that's what you want.