carlehewitt

In his famous 1936 article, Turing correctly noted that proof of the computational undecidabilty of halting problem does not involve the same fixed point as the one used by Gödel.

See the following: https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003

There is a strongly-typed definition of Y here:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003

BTW, the Church/Turing theory of computation is not universal for digital computation as explained in the following article:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003

'Setq' and 'rplacd' also do not provide the power of Actors.

See the following:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003

Schemer (later renamed Scheme) was invented to scheme against Actors reprising Conniver, which was invented to connive against Planner.

See the following for the current state of the art including the latest Actor approach to Eval, which is more modular and concurrent than the Eval in Lisp and Scheme:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003

The above article explains exactly how Actors are much more powerful than lambdas with mutable environments.

There will be zillions of different kinds of Actor in a massive inconsistency robust ontology, each with a different implementation although constructed on a common system.

Amdahl's law imposes no performance limitation on a system which does not have a sequential part. Having a sequential part is a bad idea because it is a single point of failure.

This is a very good question.

Citadels are larger scale Actors which can be incorporated into other Citadels, where a Citadel is an Actor for a systems of Actors (perhaps including IoT).

See the following:

   http://web.stanford.edu/class/ee380/Abstracts/190123.html

Every Actor has a region of mutual exclusion.

However, the region of mutual exclusion can have holes so that

    * activities can be suspended and later resumed
    * other activities can use the region of mutual
      exclusion while a message is being processed by
      another Actor

For example, a readers/writer scheduler for a database must be processing multiple activities concurrently, which is very difficult to implement in Erlang.

In a wide-ranging discussion, there were some fundamental disagreements among the panelists as follows:

I disagreed with Tony Hoare about using synchronous communication as the primitive because it is too slow for both IoT and many-core chips. Instead, the primitive for communication should be asynchronous sending and receiving, from which more complex protocols can be constructed.

Also, I disagreed with Tony about sequential actions (using ";") as being foundational. Instead, concurrent actions are foundational for digital systems as follows:

    * Receipt of a communication activated sending other communications
    * An Actor received one communication before it received another communication

Consequently, a computation is a partial order of causality. Tony and I did agree that tooling is needed for navigating the partial order. We just disagreed about whether sequential actions (using ";") are foundational.

Furthermore, class hierarchies are not a suitable foundation for Scalable Intelligent Systems. Interfaces instead of subclassing should be used for IoT communication. Also, entities and descriptions in large ontologies do not fit in an object class hierarchy, e.g., Java and C++. Subclassing is not secure because it allows a subclass to impersonate a superclass.

I disagreed with Joe Armstrong about requiring use of external mailboxes because they are inefficient in both space and time. Instead of requiring an external mailbox for each Actor, buffering/reordering/scheduling should be performed inside an Actor as required.

Of course, Tony and Joe made other great points with which we agree entirely. See the following for more information:

  http://web.stanford.edu/class/ee380/Abstracts/190123.html

The Actor Model is a formalization of what needs to be done for IoT and many-core computers. The ideas were circulating widely before work began on Erlang even if the engineers did not read the literature.

Erlang lacks holes in the region of mutual exclusion of an Actor making it very difficult to things like a readers/writer scheduler for a database.

See the following:

http://web.stanford.edu/class/ee380/Abstracts/190123.html

Actually, the Actor Model generalizes Concurrent ML because message and types are Actors.

For example, if anAccount:Account then the following

     anAccount.deposit[$5]

is defined as follows:

     Account.send[anAccount. deposit[$5]

Massive Inconsistency Robust Ontologies will have trillions of Actors on a many-core computer.

Please see the YouTube video here:

  http://web.stanford.edu/class/ee380/Abstracts/190123.html

In a wide ranging discussion, there were some fundamental disagreements among the panelists as follows:

I disagreed with Tony Hoare about using synchronous communication as the primitive because it is too slow for both IoT and many-core chips. Instead, the primitive for communication should be asynchronous sending and receiving, from which more complex protocols can be constructed.

Also, I disagreed with Tony about sequential actions (using ";") as being foundational. Instead, concurrent actions are foundational for digital systems as follows:

    * Receipt of a communication activated sending other communications
    * An Actor received one communication before it received another communication

Consequently, a computation is a partial order of causality. Tony and I did agree that tooling is needed for navigating the partial order. We just disagreed about whether sequential actions (using ";") are foundational.

Furthermore, class hierarchies are not a suitable foundation for Scalable Intelligent Systems. Interfaces instead of subclassing should be used for IoT communication. Also, entities and descriptions in large ontologies do not fit in an object class hierarchy, e.g., Java and C++. Subclassing is not secure because it allows a subclass to impersonate a superclass.

I disagreed with Joe Armstrong about requiring use of external mailboxes because they are inefficient in both space and time. Instead of requiring an external mailbox for each Actor, buffering/reordering/scheduling should be performed inside an Actor as required.

Of course, Tony and Joe made other great points with which we agree entirely.

Professor Hewitt has a blog with more info here:

   https://professorhewitt.blogspot.com/

Also related:

https://www.youtube.com/watch?v=7erJ1DV_Tlo

An Actor is not a sequential process because it does not have a program counter that moves sequentially through a program.

You might find Actors more intuitive. For example, see the following video by Hewitt, Meijer and Szyperski: The Actor Model (everything you wanted to know, but were afraid to ask)

https://channel9.msdn.com/Shows/Going+Deep/Hewitt-Meijer-and...

Induction is the most important principle for proving properties of programs.

The principle of Actor induction is:

   1. Suppose that an Actor x has property P when it is created.

   2. Further suppose that if x has property P when it receives a communication, 
      then it has property P when it has processed the communication.

   3. Then x always has the property P.

Yes, conditional critical regions can be slower because conditions can be redundantly tested.

Below is an Actor implementation of a read priority solution to the readers writers problem:

  ReadPriority[aDatabase:*ReadersWriter*]:*ReadersWriterManager*
       //  Invariant: **Nonempty** #writing# ⇨ **IsEmpty** #reading#
   **Locals**(Queue(#writersQ#, #readersQ#),
              Crowd(#reading#),
              AtMostOne(#writing#)),
   **Handlers**( 
       ⟦scheduler⟧ ↦ **As** myScheduler, // myScheduler facet of this manager
       upgrade[newVersion] ↦ 
            (**CancellAll**  #readersQ# **and** #writersQ# **and** #reading# **and** #writing#
                  **for** **Become** newVersion)
   myScheduler **implements** *ReadersWriter* **Handlers**( 
      read[aQuery] ↦ 
         **Enqueue** #readersQ# **when** **Nonempty** #writing# **or** #writersQ# **or** #readersQ# 
             **for** aDatabase.read[aQuery] **thru** #reading#
                    **permit** #readersQ#
                       **afterward** **Permit** #writersQ# **when** **IsEmpty** #reading#
                                                **else** #readersQ# **when** **IsEmpty** #writersQ#,
      write[anUpdate] ↦    
         **Enqueue** #writersQ# **when** **Nonempty** #reading# **or** #readersQ# **or** #writing# **or** #writersQ#  
              **for** aDatabase.write[anUpdate] **thru** #writing#
                   **afterward** **Permit** #readersQ# **else** #writersQ#)▮

Simulated time is not the basis of real concurrency.

Simula-67 (Dahl and Nyaaard) used co-routines in which there was no parallel execution.

Strictly speaking an Actor is not a CSP process, because an Actor does not have its own stack and does not have its own program counter that moves sequentially through a program.

Yes, Actors are faster than CSP processes with channels because there is no required overhead in communications passing through channels.

In fact, if a channel is desired it can be efficiently implemented as an Actor with put and get messages.

Instances of the induction axiom are uncountable for the higher order theory of the natural numbers, which obviously means that they cannot be enumerated using the natural numbers. However, it is very easy to use the induction axiom in proofs that are expressible using finite strings. Please see the article above published in HAL Archives.

Gödel's proposition "I'mUnprovable" cannot be constructed as a fixed point of P |-> ~|-P because ~|-P has order one greater than the order of P.

A reference is:

Ludwig Wittgenstein. 1956. Remarks on the Foundations of Mathematics, Revised Edition Basil Blackwell. 1978.

There is a discussion here:

https://hal.archives-ouvertes.fr/hal-01566393

The axioms of the higher order theory of the natural numbers are not countable and consequently not computationally enumerable. For example, there are uncountable many instances of the higher order induction axiom. Consequently, there are axioms that are not expressible as the abstractions of finite strings, just as there are real numbers that are not expressible as the abstractions of finite strings.

But proof checking is still computationally decidable by a provably total higher order procedure. See the following: https://hal.archives-ouvertes.fr/hal-01566393

The 1st order variant of the Dedekind/Peano theory of natural numbers is not suitable for computer science because it allows infinite integers and other monsters.

See the following: https://cacm.acm.org/blogs/blog-cacm/231495-what-turing-and-...

Of course, [Dedekind 1888] famously proved that the higher order theory characterized the natural numbers up to a unique isomorphism, which is impossible in the first order variant of this theory, which was developed later. Proof checking is computationally decidable in the higher order theory, which means that it is "effectively axiomatized." The fact that the theorems of the higher order theory cannot be computationally enumerated by a provably total procedure is irrelevant because, in practice, it does no good to enumerate the theorems.

Godel's results are for the 1st order variant of the Dedekind/Peano theory of the natural numbers. Consequently, there is no contradiction with the inferential completeness (every proposition is provable or disprovable) or self-provability of formal consistency in the higher order theory.

Also, Godel's proposition "I'mUnprovable" does not exist in the higher order theory because it doesn't type check.

See https://hal.archives-ouvertes.fr/hal-01566393