]>
Lambda the Ultimate - Comments
http://lambda-the-ultimate.org
CommentsenEquivalences
http://lambda-the-ultimate.org/node/5212#comment-88702
Okay, I think I have found the list of equivalences p.73, "Formalizing common sense reasoning for scalable inconsistency-robust information integration using Direct Logic Reasoning and the Actor Model":
<pre>
Substitution of equivalent propositions:
1. (Ψ⇔Φ) ⇒ (¬Ψ)⇔(¬Φ)
2. (Ψ⇔Φ) ⇒ ((Ψ ∨ Φ)⇔(Φ ∨ Φ))
3. (Ψ⇔Φ) ⇒ ((Ψ ∨ Φ)⇔(Φ ∨ Φ))
4. (Ψ⇔Φ) ⇒ ((Ψ ∧ Φ)⇔(Φ ∧ Φ))
5. (Ψ⇔Φ) ⇒ ((Ψ ∧ Φ)⇔(Φ ∧ Φ))
6. (Ψ⇔Φ) ⇒ ((Ψ ├T Φ)⇔(Φ ├T Φ))
7. (Ψ⇔Φ) ⇒ ((Φ ├T Ψ)⇔(Φ ├T Φ))
8. (Ψ⇔Φ) ⇒ ((Ψ⇒Φ)⇔(Φ⇒Φ))
9. (Ψ⇔Φ) ⇒ ((Φ⇒Ψ)⇔(Φ⇒Φ))
10. (F⇔G) ⇒ (∀F⇔∀G)
</pre>
(2 and 3) and (4 and 5) look the same, is this correct?Fri, 31 Jul 2015 21:58:31 +0000Keean SchupkeAggregations (e.g., sets) in Logic ProgramsAssociativity of ∨ is a consequence of equivalences for ∨
http://lambda-the-ultimate.org/node/5212#comment-88701
Associativity of ∨ is a consequence of equivalences for ∨.Fri, 31 Jul 2015 21:25:29 +0000HewittAggregations (e.g., sets) in Logic ProgramsDisjunctive Cases and Associativity
http://lambda-the-ultimate.org/node/5212#comment-88700
In other logics "A /\ B /\ C" is considered not well formed, and one of the conjunctions would need to be bracketed like "(A /\ B) /\ C". There are already commutativity rules (from Hewitt's comment above), should there be an associativity rule too? Fri, 31 Jul 2015 20:48:04 +0000Keean SchupkeAggregations (e.g., sets) in Logic ProgramsAggregation in Datalog
http://lambda-the-ultimate.org/node/5212#comment-88699
The Dyna language is interesting. It allows you to replace the usual nondeterministic choice | of Datalog with another operator like + or min. In normal datalog you use rules like this:
<pre>
ancestor(i,j) :- parent(i,k), ancestor(k,j)
</pre>
The rule is a disjunction over k. In Dyna you can replace conjunction and disjunction with other operators, e.g. + and * to express matrix multiply:
<pre>
A(i,j) += B(i,k)*C(k,j)
</pre>
This rule is a <i>sum</i> over k (because of += instead of -:).
Shortest paths:
<pre>
shortestPath(i,i) min= 0
shortestPath(i,j) min= edgeCost(i,k) + shortestPath(k,j)
</pre>
This is with min and +.
<a href="http://www.cs.jhu.edu/~nwf/datalog20-paper.pdf">Dyna: Extending Datalog For Modern AI</a>Fri, 31 Jul 2015 20:37:48 +0000Jules JacobsAggregations (e.g., sets) in Logic Programsword
http://lambda-the-ultimate.org/node/5209#comment-88698
Sorry above, I wasn't trying to be rude, I was just lost as to what you were asking any more. :-) I too find that the difference between how we do things in Erlang vs. ActorScript-actors-all-the-way-down is interesting, and unclear. Thanks for re-stating your question again.Fri, 31 Jul 2015 20:32:01 +0000raouldAre Actors a Good Model for Computation.re IRDL's modus ponens uses turnstile ⊢ instead of implication.
http://lambda-the-ultimate.org/node/5212#comment-88697
<blockquote>IRDL's modus ponens uses turnstile ⊢ instead of implication.</blockquote>
Modus ponens of implication is a special case of disjunctive cases.
AFAIK, chaining of arguments is a consequence of soundness.
Fri, 31 Jul 2015 19:55:35 +0000Thomas LordAggregations (e.g., sets) in Logic Programs|- vs =>
http://lambda-the-ultimate.org/node/5212#comment-88696
Yes, I was just noticing there is a difference, but I haven't fully worked it through yet. There is:
<pre>
Implication implies inference:
(⊢Τ Φ ⇒ Ψ) ⇒ Φ ⊢Τ Ψ
</pre>
but not the other way around.
Is modus ponens missing from the summery of axioms posted above, or am I just missing it for some reason?
Fri, 31 Jul 2015 19:02:36 +0000Keean SchupkeAggregations (e.g., sets) in Logic ProgramsDon't confuse IRDL's "implication" with IRDL derivability
http://lambda-the-ultimate.org/node/5212#comment-88695
In IRDL, the ⇒ implication represents a more powerful kind of derivability than IRDL's own derivability, so we can't use it in IRDL modus ponens. (IRDL's modus ponens uses turnstile ⊢ instead of implication.)
In particular, in IRDL, we can do proof by contradiction under implication, but we can't do proof by contradiction at the top level.Fri, 31 Jul 2015 18:54:35 +0000Ross AngleAggregations (e.g., sets) in Logic ProgramsWhat is it like to program?
http://lambda-the-ultimate.org/node/5209#comment-88694
Most statements in 'C' would not use the full power of actors. For example consider:
<pre>
int fact(int n) {
int x = 1;
for(int y = 2; y < n; ++y) {
x *= y;
}
return x;
}
</pre>
There is no message passing, no message order issues, the algorithm is sequential and easy to read, understand etc.
There are two different questions here:
1) Do actors provide a good internal language for compilers, which are compiling a sequential language like 'C'.
2) Do we want to write everything as actors (like everything is an object/message in smalltalk)?
In this branch of the discussion I was contrasting what 'C' is like to program in compared to actors-all-the-way-down. Does actually writing everything as an actor make it harder to write simple sequential algorithms correctly (due to message ordering etc)? If we were writing as actors we might need to instantiate the actors we want, and then plumb them together into a 'circuit'.
There is a difference between programming with actors, and the compiler using actors to model computation.
Fri, 31 Jul 2015 18:44:11 +0000Keean SchupkeAre Actors a Good Model for Computation.C could be Actors all the way down
http://lambda-the-ultimate.org/node/5209#comment-88693
C could be Actors all the way down too, with Actors for C addition.
Hewitt said elsewhere in this thread, "A goal is to model <b>all</b> digital computation using Actors. Consequently, it must be possible to model C, Erlang, etc."Fri, 31 Jul 2015 18:32:40 +0000Ross AngleAre Actors a Good Model for Computation.That's thrown me
http://lambda-the-ultimate.org/node/5212#comment-88692
I wasnt expecting that. If De Morgen is an axiom in IRDL, why can't it be used in proofs like other axioms. Are there two types of axioms?Fri, 31 Jul 2015 18:18:01 +0000Keean SchupkeAggregations (e.g., sets) in Logic ProgramsActors all the way down
http://lambda-the-ultimate.org/node/5209#comment-88691
I have written Erlang, and RPC services in 'C', so I think I understand the actor model a little bit.
My comments are around 'actors all the way down' where each actor is not a little VM that runs a 'C' program but is in turn composed of smaller actors, all the way down until you get to primitive actors, like an actor for addition at the bottom.
My understanding is ActorScript is actors all the way down, and therefore a different model from 'C' and Erlang.Fri, 31 Jul 2015 18:15:25 +0000Keean SchupkeAre Actors a Good Model for Computation.De Morgan: not allowed for proof by contradiction in IRDL
http://lambda-the-ultimate.org/node/5212#comment-88690
De Morgan does not produce implications for use in proof by contradiction in Inconsistency Robust Direct Logic.Fri, 31 Jul 2015 18:08:30 +0000HewittAggregations (e.g., sets) in Logic ProgramsWhich axioms?
http://lambda-the-ultimate.org/node/5212#comment-88689
I understand Matt's proof below, which looks correct if long. I don't understand what you mean by equivalences.
Do you mean the summary if axioms above is missing:
<pre>
A \/ B <=> B \/ A
</pre>
Fri, 31 Jul 2015 18:07:26 +0000Keean SchupkeAggregations (e.g., sets) in Logic ProgramsProve De Morgen First?
http://lambda-the-ultimate.org/node/5212#comment-88688
Okay, that's longer than I was expecting, and I have to have already proved De Morgen (in classical where its not an axiom). This is helpful.Fri, 31 Jul 2015 18:03:43 +0000Keean SchupkeAggregations (e.g., sets) in Logic Programs