Carl Hewitt

Alonzo Church

John Mccarthy

Ole-Johan Dahl

Bill Athas

Russ Atkinson

Beppe Attardi

Henry Baker

Gerry Barber

Peter Bishop

Nanette Boden

Jean-Pierre Briot

Bill Dally

Peter De Jong

Jessie Decker

Ken Kahn

Henry Lieberman

Carl Manning

Mark S Miller

Tom Reinhardt

Chuck Seitz

Dale Schumacher

Richard Steiger

Dan Theriault

Mario Tokoro

Darrell Woelk

Carlos Varela

for antiCloud privacy and security i One computer is no computer in IoT

    Copyright ActorScript™ extension of C#®, Java®, Objective C®, JavaScript®, and SystemVerilog using iAdaptive™ concurrency for antiCloud™ privacy and security

Minimize latency along critical paths ActorScript attempts to achieve the highest level of performance, scalability, and expressibility with a minimum of primitives.

Introduction

ActorScript is based on the Actor mathematical model of computation that treats "Actors" as the universal conceptual primitive of digital computation [Hewitt, Bishop, and Steiger 1973;[START_REF] Hewitt | Viewing Control Structures as Patterns of Passing Messages AI Memo 410[END_REF]Hewitt 2010a]. Actors have been used as a framework for a theoretical understanding of concurrency, and as the theoretical basis for several practical implementations of concurrent systems.

physical laws. The advent of massive concurrency through client-cloud computing and many-core computer architectures has galvanized interest in the Actor model.

An Actor is a computational entity that, in response to a message it receives, can concurrently:  send messages to addresses of Actors that it has  create new Actors  designate how to handle the next message it receives.

There is no assumed order to the above actions and they could be carried out concurrently. In addition two messages sent concurrently can be received in either order. Decoupling the sender from communication it sends was a fundamental advance of the Actor model enabling asynchronous communication and control structures as patterns of passing messages.

The Actor model can be used as a framework for modeling, understanding, and reasoning about, a wide range of concurrent systems. For example:  Electronic mail (e-mail) can be modeled as an Actor system. Mail accounts are modeled as Actors and email addresses as Actor addresses.  Web Services can be modeled with endpoints modeled as Actor addresses.  Object-oriented programing objects with locks (e.g. as in Java and C#) can be modeled as Actors.

Actor technology will see significant application for coordinating all kinds of digital information for individuals, groups, and organizations so their information usefully links together. Information coordination needs to make use of the following information system principles:  Persistence. Information is collected and indexed.

 Concurrency: Work proceeds interactively and concurrently, overlapping in time.  Quasi-commutativity: Information can be used regardless of whether it initiates new work or becomes relevant to ongoing work.  Sponsorship: Sponsors provide resources for computation, i.e., processing, storage, and communications.  Pluralism: Information is heterogeneous, overlapping and often inconsistent. There is no central arbiter of truth.  Provenance: The provenance of information is carefully tracked and recorded.

The Actor Model is designed to provide a foundation for inconsistency robust information coordination.

Notation

To ease interoperability, ActorScript uses an intersection of the orthographic conventions of Java, JavaScript, and C++ for words i and numbers.

Expressions

ActorScript makes use of a great many symbols to improve readability and remove ambiguity. For example the symbol "▮" is used as the top level terminator to designate the end of input in a readeval-print loop. An Integrated Development Environment (IDE) can provide a table of these symbols for ease of input as explained below: ii

Expressions evaluate to Actors. For example, 1+3▮ iii is equivalent iv to 4▮.

Parentheses "(" and ")" can be used for precedence. For example using the usual precedence for operators, 3(4+2)▮ is equivalent to 18▮, while 34+2▮ is equivalent to 14▮, Identifiers, e.g., x, are expressions that can be used in other expressions. For example if x is 1 then x+3▮ is equivalent to 4▮. The formal syntax of identifiers is in the following end note: 4.

Types

Types are Actors. Type names are shown as follows: o blue for types in general (e.g., Account) o green for the special case of implementation types (e.g., SimpleAccount)

The formal syntax for types is in the following end note: 5.

i sometimes called "names"

ii Furthermore, all special symbols have ASCII equivalents for input with a keyboard. An IDE can convert ASCII for a symbol equivalent into the symbol. See table in an appendix to this article. iii An IDE can provide a box with symbols for easy input in program development.

The grey callout bubble is a hover tip that appears when the cursor hovers above a symbol to explain its use. iv in the sense of having the same value and the same effects Symbols ▮ end Identifier Definitions, i.e., ← An identifier definition has an identifier to be defined followed by "←" followed by the definition. For example, x←3▮ defines the identifier x to be the Identifiers i can be bound using patterns as in the following examples:

 x is a pattern that matches "abc" and binds x to "abc" Cases, i.e., � ⦂ , ⦂ ⍰ Cases are used to perform conditional testing. In a Cases Expression, an expression for the value on which to perform case analysis is specified first followed by "�" ii and then followed by a number of cases separated by "," terminated by "⍰". 11 A case consists of  a pattern followed by "⦂" and an expression to compute the value for the case. All of the patterns before an else case must be disjoint; i.e., it must not be possible for more than one to match.  optionally (at the end of the cases) one or more of the following cases: "else" followed by an optional pattern, "⦂", and an expression to compute the value for the case. An else case applies only if none of the patterns in the preceding cases iii match the value on which to perform case analysis.

As an arbitrary example purely to illustrate the above, suppose that the procedure Random, which has no argument and returns Integer, in the following example:

Random∎[ ] � 0 ⦂ // Random∎[ ] returned 0 iv Throw v RandomNumberException[ ],
// throw an exception // because Fibonacci∎[0] is undefined 1 ⦂ // Random∎[ ] returned 1 6, // the value of the cases expression is 6 else y thatIs < 5 ⦂ // Random∎[ ] returned y that is not 0 or 1 and is less than 5 Fibonacci∎[y],

// return Fibonacci of the value returned by Random∎[ ] else z ⦂ // Random∎[ ] returned z that is not 0 or 1 and is not less than 5 Factorial∎[z] ⍰▮ // return Factorial of the value returned by Random∎[ ] The formal syntax of cases is in the following end note: 12.

i An identifier is a name that is used in a program to designate an Actor ii "�" is fancy typography for "?" iii including patterns in previous else cases iv As is standard, ActorScript uses the token "//" to begin a one-line comment. v Reserved words are shown in bold black.

Symbols

� ⦂

⍰ ▮ case Binding identifiers, i.e., ← Identifiers can be bound using an ideentifier, followed by "←" and an expression. For example, aProcedure∎["G", "F", "F"]▮ is equivalent to the following:

(x ← "F", // x is "F" aProcedure∎["G", x, x] )▮
Dependent bindings (in which each can depend on previous ones) can be accomplished as follows:

(x ← "F", // x is "F" y ← aProcedure∎["G", x, x]], // y is aProcedure∎["G", "F", "F"] anotherProcedure∎[x, y] )▮
The above is equivalent to anotherProcedure∎["F", aProcedure∎["G", "F", "F"]]▮

The formal syntax of bindings is in the following end note: 13.

The formal syntactic definition of named-message sending is in the following end note: 14 Lists, i.e., [ ] using Spread, i.e., [ ⩛ ] The prefix operator "⩛" can be used to spread the elements of a list. For example

 [1, ⩛[2, 3], 4] 15 is equivalent to [1, 2, 3, 4].  [[1, 2], ⩛[3, 4]] is equivalent to [[1, 2], 3, 4]  If y is [5, 6], then [1, 2, y, ⩛y]▮ is equivalent [1, 2, [5, 6], 5, 6]▮  [⩛[2, 3.0]]⋮⋮[Integer, Float] is equivalent to [2, 3.0]⋮⋮[Integer, Float]. i
The formal syntax of list expressions is in the following end note: 16.

i ⋮⋮ [Integer, Float] is the type of a two element list, the first of which is of type Integer and the second of type Float Symbols ← ▮ bind Within a list, "⩛"is used to match the pattern that follows with the list zero or more elements. For example:

 [[x, 2], ⩛y] is a pattern that matches [[1, 2], 3, 4] and binds x to 1 and y to ⩛x, ⩛y] is an illegal pattern because it can match ambiguously Below is the definition of a procedure that computes the reverse of a list.

[3, 4]  if y is [3, 4] then [[1, 2], ⩛⌕y] matches [[1, 2], 3, 4]  [

Define ReverseaType∎ [aList:[aType

⊛ ]]:[aType ⊛ ] ≡ aList � [ ] ⦂ [ ], [first, ⩛rest] ⦂ [⩛rest, first] ⍰▮ 17
The formal syntax of patterns is in the following end note: 18.

The following procedure returns every other element of a list beginning with the first:

Define AlternateElementsaType∎ [aList:[aType ⊛ ]]:[aType ⊛ ] ≡ aList � [ ] ⦂ [ ], [anElement] ⦂ [anElement], [firstElement, secondElement] ⦂ [firstElement], else ⦂ [firstElement, secondElement, ⩛remainingElements] ⦂ [firstElement, ⩛AlternateElements∎[remainingElements]] ⍰▮ Consequently,  AlternateElementsInteger∎[[ ]]▮ is equivalent to [ ]⋮Integer▮  AlternateElementsInteger∎[[3]]▮ is equivalent to [3]⋮Integer▮  AlternateElementsInteger∎[[3, 4]]▮ is equivalent to [3]⋮Integer▮  AlternateElementsInteger∎[[3, 4, 5]]▮ is equivalent to [3, 6]⋮Integer▮ Symbols � ⦂, ⩛   ⍰ ▮ spread Symbols → � ⦂ ← ≡ ⩛ ⍰ ▮
spread

General Message-passing interfaces

An interface can be defined using "Interface" followed by an interface name, "with", and a list of message handler signatures, where message handler signature consists of a message name followed by argument types delimited by "[" and "]", "↦", and a return type. For example, the interface type can be defined as follows:

Interface Account with availableBalance[ ]↦Euro, deposit[Euro]↦Void, withdraw[Euro]↦Void▮
Actors that change, i.e., Actor using ≔ Using the expressions introduced so far, actors do not change. However, some Actors change behaviors over time.

Message handlers in an Actor execute mutually exclusively while in a region of mutual exclusion which is called "cheese." In this paper assignable variables are colored orange, which by itself has no semantic significance, i.e., printing this article in black and white does not change any meaning. The use of assignments is strictly controlled in order to achieve better structured programs. 19 Below is a diagram for the implementation SimpleAccount of Account: Variable races are impossible in ActorScript An Actor can be created using "Actor" optionally followed by the following:  constructor name with formal arguments delimited using brackets  declarations of variables i terminated by "|"  implementations of interface(s).

ActorScript is referentially transparent in the sense that a variable never changes while in a continuous part of the cheese. 20 For example, in the deposit message handler change is accomplished using the following: Void; myBalance ≔ myBalance+anAmount which returns Void and updates myBalance for the next message received.

An implementation that of the Account interface can be expressed as follows:

Actor SimpleAccount[startingBalance:Euro] locals myBalance ≔ startingBalance| Concurrency can be controlled using preparation that is expressed in a continuation using preparatory expressions, "" and an expression that proceeds only after the preparations have been completed.

The following expression creates an account anAccount with initial balance €6 and then concurrently withdraws €1 and €2 in preparation for reading the balance:

(anAccount ← SimpleAccount[€6],
// € is a reserved prefix operator anAccount∎withdraw[€1] ⫼ anAccount∎withdraw[€2] // proceed only after both of the // withdrawals have been acknowledged

anAccount∎availableBalance[ ])▮

The above expression returns €3.

Operations are quasi-commutative to the extent that it doesn't matter in which order they occur.

Quasi-commutativity can be used to tame indeterminacy while at the same time facilitating implementations that run exponentially faster than those in the parallel lambda calculus. i

The formal syntax of compound expressions is in the following end note: 22

An expression can be annotated for concurrent execution by preceding it with "℗" indicating that the following expression must be considered for parallel The formal syntax of explicit concurrency is in the following end note: 24.

i For example, implementations using Actors of Direct Logic can be exponentially faster than implementations in the parallel lambda calculus.

Symbols  ← € ▮ Euro
Implementing multiple interfaces , i.e., also implements

The above implementation of Account can be extended as follows to provide the ability to revoke 25 some abilities to change an account. 26 The formal syntax of the programs below is in the following end note: 30

Type Extension

Subtyping of an implementation is not allowed so that an implementation can be securely branded. i The following interface expresses that each Tree has an integer identifier:

Interface Tree with ⟦hash⟧↦Integer▮ Testing for convertibility from of a type to an extension of the type is done using an expression of the extension can followed by "↓?" and the type. For example,  ((Leaf ["The"]):Tree)↓?Fork▮ is equivalent to False▮.  ((Leaf ["The"]):Tree)↓?Leaf ▮ is equivalent to True▮.

Conversion from of a type to an extension of the type is done using an expression of the extension can followed by "↓" and the type. For example,  ((Leaf ["The"]):Tree)↓Leaf ▮ is equivalent to Leaf ∎["The"]▮.  ((Leaf ["The"]):Tree)↓Fork▮ throws an exception.

"⟐⟐↓" followed by a pattern can be used to match the pattern with something which has been extended from the type of that pattern. For example, 31 Define Fringe∎[aTree:Tree]:

[String ⊛ ] ≡ aTree � ⟐⟐↓Leaf[aString] ⦂ [aString], ⟐⟐↓Fork[left, right] ⦂ [⩛Fringe∎[left], ⩛Fringe∎[right]] ⍰▮ Symbols → � ⦂ ← ⩛ ≡ ⍰ ▮ definition
For example, ["The", "boy"]⋮String▮ is equivalent to the following:

Fringe∎[Fork [Leaf["The"], Leaf["boy"]]]▮ 32
The procedure Fringe can be used to define SameFringe? that determines if two trees have the same fringe [Hewitt 1972]: Define SameFringe?∎[aTree:Tree, anotherTree:Tree]:Boolean ≡ // test if two trees have the same fringe

Fringe∎[aTree] = Fringe∎[anotherTree]▮
Casting is as allowed only as follows:

1. Casting self to an interface implemented by this Actor 2. Upcasting a. an Actor of an implementation type to the interface type of the implementation b. an Actor of an interface type to the interface type that was extended c. an Actor to a restricted interface of the Actor 3. Conditional downcasting of an Actor of an interface type to an extension of the interface type. i Downcasting of an interface type I is allowed only to an extension of I. For example, if x is of interface type I, then either i. E is an extension of I and there is some y of type E such that x=y:I and therefore x↓E=y ii. x↓E throws an exception because E is not an extension of I or there is no y of type E such that x=y:I

Swiss cheese

Swiss cheese [Hewitt andAtkinson 1977, 1979;Atkinson 1980] By the Actor Model of Computation [START_REF] Clinger | Foundations of Actor Semantics MIT Mathematics Doctoral Dissertation[END_REF][START_REF] Hewitt | What is Commitment? Physical, Organizational, and Social" COIN@AAMAS'06[END_REF], the above Actor will eventually receive the stop[ ] message and return an unbounded number.

A diagram is shown below for an implementation of Counter. In the diagram, a hole in the cheese is highlighted in grey and variables are shown in orange.

The color has no semantic significance. The above example illustrates how nondeterministic branching (in Turing Machines) is not a good model for message reception in IoT.

The formal syntax of the programs above is in the following end note: 34

Symbols → � ⦂ ⍰ ¶ § ▮

Coordinating Activities

Coordinating activities of readers and writers in a shared resource is a classic problem. The fundamental constraint is that multiple writers are not allowed to operate concurrently and a writer is not allowed operate concurrently with a reader.

Below are two implementations of readers/writer guardians for a shared resource that implement different policies: 35 1. ReadingPriority: The policy is to permit maximum concurrency among readers without starving writers. 36 a. When no writer is waiting, all readers start as they are received. b. When a writer has been received, no more readers can start. c. When a writer completes, all waiting readers start even if there are writers waiting. 2. WritingPriority: The policy is that readers get the most recent information available without starving writers. 37 a. When no writer is waiting, all readers start as they are received. b. When a writer has been received, no more readers can start. c. When a writer completes, just one waiting reader is permitted to complete if there are waiting writers. Note:

1. At most one activity is allowed to execute in the cheese.

2. The value of a variable i changes only when leaving the cheese. ii

When an exception is thrown exogenously by an activity that is in a queue (e.g., readersQ, writersQ), a backout handler can be used to clean up cheese variables before rethrowing the exception.

The formal syntax of the programs below is in the following end note:

38 i A
Symbols → � ⦂    ⍰ ¶ § ▮

Conclusion

By the time the Software Engineering of a language gets in good shape, the language has become obsolete in "needed expressiveness"! Alan Kay 40 Before long, we will have billions of chips, each with hundreds of hyperthreaded cores executing hundreds of thousands of threads. Consequently, GOFIP (Good Old-Fashioned Imperative Programming) paradigm must be fundamentally extended. ActorScript is intended to be a contribution to this extension.

ActorScript has been designed for use with a TIDE (Team Integrated Development Environment). Implementation is the next task before us!

The members of the Silicon Valley Friday AM group made valuable suggestions for improving this paper. Discussions with Blaine Garst were helpful in the development of the implementation of Swiss cheese that doesn't hold a lock as well providing background on the historical development of interfaces. Patrick Beard found bugs and suggested improvements in presentation. Fanya S. Montalvo and Ike Nassi suggested simplifying the syntax. Dale Schumacher found many typos, suggested including a syntax diagram, and suggested improvements to the syntax of collections, binding and assignment. In particular, Dale contributed greatly to the development of the lock-free i implementation of cheese in the appendix. Chip Morningstar provided an excellent critique with many useful comments and suggestions. Many important comments and suggestions were provided by Stu Bailey and members of the Silicon Valley FriAM group.

ActorScript is intended to provide a foundation for information coordination in client-cloud computing that protects citizens sensitive information [Hewitt 2009b].

Bibliography

type parameter

Type Discrimination, i.e., Discrimination ↑ and ↓ A discrimination definition is a type of alternatives differentiated by type using "Discrimination" followed by a type name, "between", types separated using "," terminated by "▮".

A discrimination can constructed using an expression followed by "↑" and the discrimination type. A discrimination can be tested if it holds a discrimination of a certain type with an expression for the discrimination followed by "↓?" and the type to be tested. An expression for a discrimination followed by "↓" and a type is the discriminate of that type.

For example, consider the following definition:

Discrimination IntegerOrString between Integer, String▮

Consequently,  (3↑IntegerOrString)↓Integer▮ is equivalent to 3▮.  ("a"↑IntegerOrString) ↓Integer▮ throws an exception because String is not the same as the discriminant Integer.

 (3↑IntegerOrString) ↓?Integer▮ is equivalent to True▮.  (3↑IntegerOrString) ↓?String▮ is equivalent to False▮.  [3↑IntegerOrString, "a"↑IntegerOrString]⋮IntegerOrString is of type [IntegerOrString ⊛ ]
A pattern followed by "⟐↓"and the type to be projected matches an Actor if the pattern matches the projection.  The pattern x⟐↓String matches "a"↑IntegerOrString and binds x to "a".  The pattern x⟐↓String does not match 3↑IntegerOrString  The expression below is equivalent to 2▮:

3↑IntegerOrString � y↓Integer ⦂ y-1, x↓String ⦂ x ⍰▮
Discriminations can also be used in crypto as in the following definition: Discrimination EmployeeNumberOrEncrypted between EmployeeNumber, Encrypted▮ with the result that having an address x of type EmployeeNumberOrEncrypted does not by itself provide access to an encrypted employee number from x without also having the type EmployeeNumber using DecryptEmployeeNumber∎ [x↓Encrypted] The formal syntax of type discrimination is in following end note: 42.

Structures

A structure is an Actor used in pattern matching that can be defined using an identifier by "[", parts separated by "," and "]".

Discrimination can be used with structures. For example, a TrieaType is a discrimination of TerminalaType and TrieForkaType:

Discrimination TrieaType between TerminalaType, TrieForkaType▮

where the structure Terminal can be defined as follows:

Structure TerminalaType[anActor:aType]▮

For example,  The expression

(x i ← 3, TerminalInteger[x] )▮ is equivalent to TerminalInteger[3]▮  The pattern TerminalInteger[x] matches TerminalInteger[3]
and binds x to 3.

The structure TrieFork can be defined as follows:

Structure "⟐⟐↓" followed by a structure pattern an Actor if the pattern matches the projection.

i x is of type Integer Below is the definition of a procedure that computes a list that is the "fringe" of the terminals of a Trie. i

Define TrieFringeaType∎[aTrie:TrieaType

]:[aType ⊛ ] ≡ aTrie � ⟐⟐↓TerminalaType[x] ⦂ [x], ⟐⟐↓TrieForkaType[left, right] ⦂ [⩛TrieFringe∎[left], ⩛TrieFringeaType∎[right]] ⍰▮
The above procedure can be used to define TrieSameFringe? that determines if two lists have the same fringe [Hewitt 1972 In an expression,  "•" followed by an expression of type NullableaType is the Actor (of type aType) in the nullable or throws an exception if there is no Actor.  "Nullable" followed by an expression of type aType is the nullable (of type NullableaType) containing the value of the expression.  "Null" followed by a type is the null for that type. In a pattern,  "⟐•" followed by a pattern matches a nullable if and only if it is non-null and the pattern matches the Actor in the nullable.  TheNull only matches the null. The formal syntax of processing exceptions is in the following end note: 46.

Runtime Requirements, i.e., precondition and postcondition A runtime requirement throws exception an exception if does not hold. For example, the following expression throws an exception that the requirement x0 doesn't hold:

(x ← -1, x0 precondition SquareRoot∎[x] )▮
Post conditions can be tested using a procedure. For example, the following expression throws an exception that postcondition failed because square root of 2 is not less than 1:

SquareRoot∎[2] postcondition λ [y:Float]:Boolean → y<1▮
The formal syntax requirements is in the following end note: 47.

Multiple implementations of a type

The interface type Complex is defined as follows:

Interface Complex with ⟦real⟧ |••> Float, ⟦imaginary⟧ |••> Float, ⟦magnitude⟧ |••> Float, ⟦angle⟧ |••> Degrees▮
Cartesian Actors that implement Complex can be defined as follows:

Structure The formal syntax of named arguments is in the following end note: 52.

Symbols → ⌸ ⍰ ¶ § ▮ keyword argument
Sets, i.e., { } using spreading, i.e., { ⩛ } A set is unordered with duplicates removed.

The formal syntax of sets is in the following end note: 53.

Multisets, i.e., ⦃ ⦄ using spreading, i.e., ⦃ ⩛ ⦄ A set is unordered with duplicates allowed.

The formal syntax of multisets is in the following end note: 54.

Maps,

A map is composed of pairs. For example, the following is a map:

MapInteger, String[[3]↠"a", [4]↠"b"] ▮
Pairs in maps are unordered, e.g.,

MapInteger, String[[3]↠"a", [4]↠"b"]▮ is equivalent to MapInteger, String[[4]↠"a", [3]↠"b"]▮.
However, the expression MapInteger, String[[4]↠"a", [4]↠"b"]▮ throws an exception because a map is univalent.

The formal syntax of multisets is in the following end note: 55.

As another example, for the contact records of 1.1 billion people, the following can compute a list of pairs from age to average number of social contacts of US citizens sorted by increasing age making use of the following:

Structure ContactRecord[yearsOld:Age⌸, numberOfContacts:Integer⌸, citizenship:String⌸]▮ [ContactRecord ⊛ ] has filter[[ContactRecord] |••> Boolean] |••> {ContactRecord ⊛ }, collect [[ContactRecord] |••> [Age, Integer]] |••> MapAge, {Integer ⊛ }▮ MapAge, {Integer ⊛ }  has reduceRange[[{Integer ⊛ }] |••> Float] |••> MapAge, Float▮ {Number ⊛ } has average[ ] |••> Float▮ MapAge, Float has sort[[Age, Age] |••> Boolean] |••> [Age, Float]▮ The program is a follows: 56 Define AgeWithAverageOfNumberOfContactsSortedByAge∎ [records:{ContactRecord ⊛ }]:SortedAge ≡ records∎filter [[aRecord:ContactRecord] ••> aRecord∎⟦citizenship⟧ � "US" ⦂ True, else ⦂ False ⍰] ∎collect [[aRecord:ContactRecord] ••> [aRecord∎⟦yearsOld⟧, aRecord∎⟦numberOfContacts⟧] ∎reduceRange [[aSetOfNumberOfContacts:{Integer ⊛ }] ••> aSetOfNumberOfContacts∎average[ ]] ∎sort[LessThanOrEqualAge]▮

Encryption

Actor addresses can be type-encrypted using Encrypt. Using the above definition, the following is a contact record with fields yearsOld, numberOfContacts, and citizenship type encrypted:

Encrypt ContactRecord[yearsOld ⌸ 5, numberOfContacts ⌸ 7, citizenship ⌸ "UK"]▮ 57

The above encrypted contact record can be decrypted only by using the type ContactRecord. For example, the encrypted record above matches the following pattern: DecryptedContactRecord aRecord with aRecord bound to the decrypted record.

Futures, i.e., Future and •

A future [Baker and [START_REF] Hewitt | Viewing Control Structures as Patterns of Passing Messages AI Memo 410[END_REF] for an expression can be created in ActorScript by using "Future" preceding the expression. The operator "•" can be used to "reduce" a future by returning an Actor computed by the future or throwing an exception. For example, the following expression is equivalent to Factorial∎[9999]▮ (aFuture i ←Future Factorial∎[9999],

•aFuture)▮ The formal syntax of language extension is in the following end note: 61.

i this is allowed because postponed is of type aType

In-line Recursion (e.g., looping) , i.e. Loop ∎[ ← , ← ] is

Inline recursion (often called looping) is accomplished using "Loop", an initial invocation with identifiers initialized using "←" followed by "is" and the body. i

Below is an illustration of a loop Factorial with two loop identifiers n and accumulation. The loop starts with n equals 9 and value equal 1. The loop is iterated by a call to Factorial with the loop identifiers as arguments.

Loop Factorial∎[n ← 9, accumulation ← 1] is n=1 � True ⦂ accumulation, False ⦂ Factorial∎[n-1, n accumulation] ⍰▮ ii
The above compiles as a loop because the call to Factorial in the body is a "tail call" [START_REF] Hewitt | More Comparative Schematology MIT AI Memo 207[END_REF][START_REF] Hewitt | Viewing Control Structures as Patterns of Passing Messages AI Memo 410[END_REF][START_REF] Steele | Debunking the 'Expensive Procedure Call' Myth, or, Procedure Call Implementations Considered Harmful, or, Lambda: The Ultimate GOTO[END_REF].

The following expression returns a list of ten times successively calling the parameterless procedure

P iii (of type [ ]↦ Integer): Loop FirstTenSequentially∎[n ← 10] is n=1 � True ⦂ [P∎[ ]], False ⦂ (x ← P∎[ ] [x, ⩛FirstTenSequentially∎[n-1]] )⍰▮
The following returns one of the results of concurrently calling the procedure P iv (which has no arguments and returns Integer) ten times with no arguments:

Loop OneOfTen∎[n ← 10] is n=1 � True ⦂ P∎[ ], False ⦂ ℗P∎[ ] either ℗OneOfTen∎[n-1]] ⍰▮ 62
The formal syntax of looping is in the following end note: 63.

i This construct is used instead of while, for, etc. loops used in other programming languages. ii equivalent to the following:

Loop Factorial∎[n:Integer ← 9, accumulation:

Integer ← 1]:Integer is n=1 � True ⦂ accumulation, False ⦂ Factorial∎[n-1, naccumulation] ⍰▮

Strings

Strings are Actors that can be expressed using """, string arguments, and """. For example,  ""1", "23", "4""▮ is equivalent to "1234"▮.

 ""1", "2", "34", "56""▮ is equivalent to "123456"▮.  " ""1", "2"", "34""▮ is equivalent to "1234"▮.

 " "▮ is equivalent to ""▮.

String patterns are delimited by """ and """. Within a string pattern, "⩛" is used to match the pattern that follows with the list zero or more characters. For example:  "x, "2", ⩛y" is a pattern that matches "1234" and binds x to "1" and y to "34".  ""1", "2", ⩛⌕y" is a pattern that only matches "1234" if y is "34".  "⩛x, ⩛y" is an illegal pattern because it can match ambiguously.

As an example of the use of spread, the following procedure reverses a string: 64 Define Reverse∎[aString:String]:String ≡ aString � " " ⦂ " " , "first, ⩛rest" ⦂ "⩛rest, first" ⍰▮

The formal syntax of string expressions is in the following end note: 65.

General Messaging, i.e., ∎ and ⨀ The syntax for general messaging is to use an expression for the recipient followed by "∎" and an expression for the message.

For example, if anExpression is of type ExpressionInteger then, anExpression∎eval[anEnvironment]▮ is equivalent to the following:

(aMessage ← eval⨀ExpressionInteger[anEnvironment], anExpression∎aMessage)▮

The formal syntax of general messaging is in the following end note: 66. The formal syntax of atomic operations is in the following end note: 68.

i Interface Lockable with lock[ ]↦ Void, unLock[ ]↦ Void▮ Symbols → � ⦂ ⍰ ¶ § ▮
The following is an implementation of an arithmetic logic unit that implements jumpGreater and addJumpPositive one-way messages:

Actor

SubArguments

This section explains how subarguments i can be implemented in natural deduction.

When ⊩s (psi ⊢t phi) → (t' ← Extension∎[t],

⊢t' psi ⫼ ⊩t' phi → ⊢s (psi ⊢t phi ))▮ Note that the following hold for t' because it is an extension of t:

 when ⊢t theta → ⊢t' theta ▮  when ⊩t' theta → ⊩t theta ▮ i See appendix on Inconsistency Robust Natural Deduction.

Construct i is the fundamental type for ActorScript programming language constructs. ExpressionaType is an extension of Construct with an eval message that has an environment with the bindings of program identifiers and a message with an environment and cheese:

Interface ,11,13,18,21,22,47,76,81,85 §,11,84 ¶,11 ¶,84 ℗,12,18,69,84 ⦂,7,84 Activity,82 Actor,11,13,18,21,52,79 ,57,63 Simi,M.,23 Smith,S.,23 Steiger,R.,23 Structure,14,15,38,39 Suspend,81,83,86 Swiss cheese,16 Symbols,84 Talcott,C.,23 Terminal,35 Thati,P.,23 thatIs,7,86 TheNull,37,67,86 Theriault,D.,23 This (JavaScript),48 threw,86 Threw,52 throw,57 Throw,11,37 Tokoro,M.,23 Tree,14,15 Trie,35 TrieFork,35 True,86 Try,37,86 Try ... catch�,72 Try ... cleanup :Expression ▮ // Execute anExpression in parallel and respond with the outcome. // In every case, anExpression must complete before execution leaves // the lexical scope in which it appears.

25 cf. [START_REF] Crahen | Facet: A pattern for dynamic interfaces[END_REF], Amborn 2004[START_REF] Miller | Bringing Object-orientation to Security Programming[END_REF] 26 The ability to extend implementation is important because it helps to avoid code duplication.

27 note the absence of "∎" in the implementation subexpression 28 equivalent to the following:

myBalance⨀SimpleAccount ≔ myBalance⨀SimpleAccount -anAmount 29 ignoring exceptions in this way is not a good practice

  The interface for the readers/writer guardian is the same as the interface for the shared resource:Interface ReadersWriter with read[Query]↦ QueryAnswer, write[Update]↦ Void▮Cheese diagram for ReadersWriter implementations:

  TrieForkaType[left:TrieaType, right:TrieaType] flip[ ]:TrieForkaType → // flip the branches TrieForkaType[right, left]▮ For example,  The expression (x ← 3, TrieFork[Terminal[x], Terminal[x+1]] )▮ 43 is equivalent to the following: TrieFork[Trie[Terminal[5], Trie[Terminal[6]]▮  The pattern TrieForkInteger[x, y] matches TrieFork[Trie[Terminal[5], Trie[Terminal[6]]▮ and binds x to Terminal[5] and y to Terminal[6].

  ]: Define TrieSameFringe?aType∎[left:TrieaType, right:TrieaType]:Boolean ≡ // test if two Tries have the same fringe TrieFringeaType∎[left] = TrieFringeaType∎[right]▮ The formal syntax of structures is in the following end note: 44 Nullable Distinguishing a special case to indicate the absence of an Actor is a long-time issue [Hoare 2009].

  For example,  Nullable 3 is of type NullableInteger  •Nullable 3▮ is equivalent to 3▮  •Null Integer▮ throws an exception i See definition of Trie above in this article.



  The pattern ⟐•x matches Nullable 3, binding x to 3  The pattern ⟐•x does not match Null Integer  The pattern TheNull matches Null Integer The formal syntax of nullables is in following end note: 45. Processing Exceptions, i.e., Try catch� ⦂ , ⦂ ⍰ and Try cleanup It is useful to be able to catch exceptions. The following illustration returns the string "This is a test.": Try Throw Exception["This is a test."] catch� Exception[aString] ⦂ aString ⍰▮ The following illustration performs Reset∎[ ] and then rethrows Exception["This is another test."]: Try Throw Exception["This is another test."] cleanup Reset∎[ ]▮

  Imposes no overhead on implementation of Actor systems in the sense that ActorScript programs are as efficient as the same implementation in machine code. For example, message passing has essentially the same overhead as procedure calls and looping.

	 Safety, security and readability
	o	Programs are extension invariant, i.e., extending a program does
		not change the meaning of the program that is extended.
	o	Applications cannot directly harm each other.
	o	Variable races are eliminated while allowing flexible
		concurrency.
	o	Lexical singleness of purpose. Each syntactic token is used for
		exactly one purpose.
	 Performance i
	o
	o	Execution dynamically adjusted for system load and capacity
		(e.g. cores)
	o	Locality because execution is not bound by a sequential global
		memory model
	o	Inherent concurrency because execution is not limited by being
		restricted to communicating sequential processes
	o

  Define CreateUnbounded∎[ ]:Integer ≡ (aCounter ← Counter ∎[ ], // let aCounter be a new Counter ℗aCounter∎go[ ] ⫼ // send aCounter a go message and concurrently ℗aCounter∎stop[ ])▮ // return the result of sending aCounter stop[ ] As a notational convenience, when an Actor receives message then it can send an arbitrary message to itself by prefixing it with "∎∎" as in the following example for the Actor implementation Counter:

	Actor Counter[ ]
	locals count ≔ 0,	// the variable count is initially 0
	continue ≔ True|
	stop[ ]:Integer → count ↺ continue ≔ False ¶

// return count; afterward continue is updated to // False for the next message received go[ ]:Void → continue � True ⦂ (count ≔ count+1, // increment count hole ∎∎go[ ]), // send go[ ] to this counter False ⦂ Void ⍰ §▮ // if continue is False, return Void As a result of the above definition Implementation Counter has go[ ]↦ Void, stop[ ]↦ Integer▮

  variable is orange in the diagram ii Of course, other external Actors can change. 21In the implementations below, preconditions present are commentary for error checking. An exception is thrown if a precondition is not met at runtime. A precondition has no operational effect.

	Illustration of writing-priority:
	Actor WritingPriority[theResource:ReadersWriter]
	invariants numberReading≧0, writing⇨numberReading=0|
	queues readersQ, writersQ| Actor ReadingPriority[theResource:ReadersWriter] locals writing ≔ False, invariants numberReading≧0 ,writing⇨ numberReading=0| queues readersQ, writersQ| numberReading ≔ 0| // readersQ and writersQ are initially empty implements ReadersWriter using locals writing ≔ False, numberReading: ≔ 0| implements ReadersWriter using read[aQuery:Query]:QueryAnswer → read[aQuery:Query]:QueryAnswer → Symbols ((writing  Empty writersQ) � → � ⦂    True ⦂ Enqueue readersQ // release cheese while in readersQ ⍰ ¶ § ▮ backout writing  numberReading=0  IsEmpty readersQ �
		True ⦂ Void permit writersQ,
		False ⦂ Void ⍰
	Void, False ⦂ Void ⍰ Void, writing precondition True ⦂ Void permit writersQ, False ⦂ Void ⍰
	False ⦂ Void ⍰
	writing
		True ⦂ Void permit readersQ,
		False ⦂ Void ⍰
	Void,	True ⦂ Void permit readersQ,
	False ⦂ Void ⍰	False ⦂ Void ⍰
	Void, numberReading=0  writing precondition False ⦂ Void ⍰ // commentary for error checking
	numberReading=0  writing precondition (writing ≔ True
	// commentary for error checking hole theResource∎write[anUpdate] // release cheese for writing
	(writing ≔ True ↺ (IsEmpty readersQ) �	// record that writing is happening // after writing if readersQ is empty
	hole theResource∎write[anUpdate] True ⦂ Permit writersQ also writing ≔ False, // release cheese for writing
	↺ (IsEmpty readersQ) � True ⦂ Permit writersQ also writing ≔ False, // after writing if readersQ is empty False ⦂ Permit readersQ also writing ≔ False⍰) §▮
	False ⦂ Permit readersQ also writing ≔ False⍰) §▮

((writing  IsEmpty writersQ) � True ⦂ Enqueue readersQ // release cheese while in readersQ backout (writing  numberReading=0  IsEmpty readersQ) � // commentary for error checking (numberReading++ // increment numberReading permit readersQ hole theResource∎read[aQuery] // release cheese for reading ↺ (IsEmpty writersQ) � // after releasing if writersQ is empty True ⦂ Permit readersQ, 39 False ⦂ numberReading=1 � True ⦂ Permit writersQ also numberReading--, False ⦂ numberReading--⍰ ⍰) ¶ write[anUpdate:Update]:Void → ((numberReading>0  IsEmpty readersQ  writing  IsEmpty writersQ) � True ⦂ Enqueue writersQ // release cheese while in writersQ backout (IsEmpty writersQ  writing) � // commentary for error checking (numberReading++ permit IsEmpty writersQ � True ⦂ readersQ, False ⦂ Void ⍰ hole theResource∎read[aQuery] // release cheese for reading ↺ (IsEmpty writersQ) � // after reading if writersQ is empty True ⦂ Permit readersQ, False ⦂ numberReading=1 � True ⦂ Permit writersQ also numberReading--, False ⦂ numberReading--⍰ ⍰) ¶ write[anUpdate:Update]:Void → ( (numberReading>0  IsEmpty readersQ  writing  IsEmpty writersQ)� True ⦂ Enqueue writersQ // release cheese while in writersQ backout (IsEmpty writersQ  writing) �

  Hal Abelson and Gerry Sussman Structure and Interpretation of Computer Programs 1984. Paul Abrahams. A final solution to the Dangling else of ALGOL 60 and related languages CACM. September 1966. Sarita Adve and Hans-J. Boehm Memory Models: A Case for Rethinking Parallel Languages and Hardware CACM. August 2010. Mikael Amborn. Facet-Oriented Program Design. LiTH-IDA-EX-04/047-SE Linkőpings Universitet. 2004. Joe Armstrong History of Erlang HOPL III. 2007. Joe Armstrong. Erlang. CACM. September 2010/ William Athas and Charles Seitz Multicomputers: message-passing concurrent computers IEEE Computer August 1988. William Athas and Nanette Boden Cantor: An Actor Programming System for Scientific Computing in Proceedings of the NSF Workshop on Object-Hewitt (2009b) A historical perspective on developing foundations for client-cloud computing: iConsult TM & iEntertain TM Apps using iInfo TM Information Integration for iOrgs TM Information Systems (Revised version of "Development of Logic Programming: What went wrong, What was done about it, and What it might mean for the future" AAAI Workshop on What Went Wrong. AAAI-08.) ArXiv 0901.4934.The formal syntax of parameterized types is in the following end note: 41 .

	Appendix 1. Extreme ActorScript
	Parameterized Types, i.e.,  , 
	Carl Hewitt (2013) Inconsistency Robustness in Logic Programs Carl Hewitt (2010b) iTooling™: Concurrency // addition for aType that is Arithmetic Infrastructure for iAdaptive TM [x:aType]:aType → aType[x+x] §▮ College Publications. 2015. Actor DoubleaType⊒Arithmetic Carl Hewitt (2010a) Actor Model of Computation Inconsistency Robustness. "": Inconsistency Robustness. College Publications. 2015. Symbols Parameterized Types are specialized → ↦ ▮ using other types delimited by "" and  
	Carl Hewitt (editor). Inconsistency Robustness 1011 Stanford University. Parameterized Types have become increasingly important. For example, the 2011. following is adapted from [Greenman, Muehlboeck, and Tate 2014]: Carl Hewitt, Erik Meijer, and Clemens Szyperski "The Actor Model (everything you wanted to know, but were afraid to ask)" Interface GraphGraph, Edge, Vertex
	with ⟦vertices⟧ ↦ [Vertex ⊛ ]▮
	Interface EdgeGraph, Edge, Vertex
	with ⟦graph⟧ ↦ Graph,
	⟦source⟧ ↦ Vertex,
	⟦target⟧ ↦ Vertex▮
	Interface VertexGraph, Edge, Vertex	World Scientific Publishing
	Company. 2012. with ⟦graph⟧ ↦ Graph, Based Concurrent Programming. 1988. Special Issue of SIGPLAN Tony Hoare Quick sort Computer Journal 5 (1) 1962. ⟦incoming⟧ ↦ [Edge ⊛ ], Notices. Russ Atkinson. Automatic Verification of Serializers MIT Doctoral Tony Hoare Monitors: An Operating System Structuring Concept CACM. ⟦outgoing⟧ ↦ [Edge ⊛ ]▮ October 1974. Dissertation. June, 1980. Henry Baker. Actor Systems for Real-Time Computation MIT EECS Doctoral Dissertation. January 1978. Tony Hoare. Communicating sequential processes CACM. August 1978. Actor GeoMap[ ] Tony Hoare. Communicating Sequential Processes Prentice Hall. 1985. Tony Hoare. Null References: The Billion Dollar Mistake. QCon. August implements GraphGeoMap, Road, Intersection using ...▮ Henry Baker and Carl Hewitt The Incremental Garbage Collection of Processes Proceeding of the Symposium on Artificial Intelligence 25, 2009. W. Horwat, Andrew Chien, and William Dally. Experience with CST: Actor Road[ ] implements EdgeGeoMap, Road, Intersection using ...▮ Programming Languages. SIGPLAN Notices 12, August 1977. Paul Baran. On Distributed Communications Networks IEEE Transactions on Communications Systems. March 1964. M. Jammer The EPR Problem in Its Historical Development in Symposium Gerry Barber. Reasoning about Change in Knowledgeable Office Systems Programming and Implementation PLDI. 1989. Actor Intersection[ ] implements Anthony Hunter. Reasoning with Contradictory Information using Quasi-classical Logic Journal of Logic and Computation. Vol. 10 No. 5. 2000. VertexGeoMap, Road, Intersection using ...▮
	MIT EECS Doctoral Dissertation. August 1981. on the Foundations of Modern Physics: 50 years of the Einstein-Podolsky-Philippe Besnard and Anthony Hunter. Quasi-classical Logic: Non-Rosen Gedankenexperiment, edited by P. Lahti and P. Mittelstaedt. World trivializable classical reasoning from inconsistent information Symbolic and Quantitative Approaches to Reasoning and Uncertainty. Springer Scientific. Singapore. 1985. LNCS. 1995. Simon Peyton Jones, Andrew Gordon, Sigbjorn Finne. Concurrent Haskell, Peter Bishop Very Large Address Space Modularly Extensible Computer POPL'96. Systems MIT EECS Doctoral Dissertation. June 1977. Ken Kahn. A Computational Theory of Animation MIT EECS Doctoral
	Dissertation. August 1979.

i In the sense that the implementation holds a hardware lock. Carl http://channel9.msdn.com/Shows/Going+Deep/Hewitt-Meijer-and-Szyperski-The-Actor-Model-everything-you-wanted-to-know-but-wereafraid-to-ask Microsoft Channel 9. April 9, 2012. Carl Hewitt. "Health Information Systems Technologies" http://ee380.stanford.edu/cgibin/videologger.php?target=120606-ee380-300.asx Slides for this video: http://HIST.carlhewitt.info Stanford CS Colloquium. June 6, 2012. Carl Hewitt. What is computation? Actor Model versus Turing's Model in "A Computable Universe: Understanding Computation & Exploring Nature as Computation". edited by Hector Zenil.

  / perform the loop Attempt as follows Atomic locked compare False update True � // attempt to atomically update locked from False to True updated ⦂ locked=True precondition // commentary for error checking: // locked must have contents True Void, // if updated return Void notUpdated ⦂ Attempt∎[ ] ⍰ ¶ // if not updated, try again unLock[ ]:Void → locked =True precondition // commentary for error checking: // locked must have contents True Void ↺ locked ≔ False §▮ // reset locked to False

	Atomic Operations, i.e. Atomic compare update updated notUpdated
	For example, the following example implements a lockable that spins to
	lock: 67
	Actor SpinLock[ ]
	locals locked ≔ False|	// initially unlocked
	implements Lockable i using
	lock[ ]:Void →
	Loop Attempt∎[ ] is
		Symbols
		� ⦂ ⩛
		⍰ ¶ § ▮

/

  Male and Human 74 ⟦magnitude⟧:Meter → (⍠Male)∎⟦length⟧ ¶ // using this Actor with Male interface ⟦length⟧:Year → (⍠Human)∎ ⟦magnitude⟧ §▮

	Using multiple other implementations , i.e., ⍠ Illustration of backward chaining:
	one-way message send This section presents an example of using multiple other ⊢t Human[Socrates]▮ When ⊩t Mortal[x] → (⊩t Human[⌕x] → ⊢t Mortal[x])▮ implementations such as the ones below: ⊩t Mortal[Socrates]▮ Symbols ⍰ ¶ § ▮ ⟦length⟧:Meter → aLength §▮ □ � ⦂ Actor Male[aLength:Meter] will result in asserting Mortal[Socrates] for theory t.
	Actor Human[aMagnitude:Year] ArithmeticLogicUnitaType[] implements ALUaType using ⟦magnitude⟧:Year → aMagnitude §▮
	jumpGreater[x:aType, y:aType,
	firstGreaterAddress:Address, elseAddress:Address]:⊝ → Boy below makes use of both the Male and Human implementations:
	InstructionUnit□Execute[(x>y) �
	True ⦂ firstGreaterAddress, Actor Boy[aMagnitude:Meter, aLength:Year]
	False ⦂ elseAddress ⍰] ¶ addJumpPositive[x:aType, y:aType, sumLocation:LocationaType, uses Male[aMagnitude], Human[aLength] |
	positiveAddress:Address, elseAddress:Address]:⊝ →
	(z ← (x+y),
	sumLocation �
	aVariableLocation:VariableLocationaType i ⦂
	(VariableLocation∎store[z]
	// continue after acknowledgement of store
	(z >0) � True ⦂ InstructionUnit□execute[positiveAddress],
	False ⦂ InstructionUnit□execute[elseAddress] ⍰),
	aTemporaryLocation:TemporaryLocationaType ii ⦂
	(aTemporaryLocation□write[z] ⫼
	// continue concurrently with processing write
	(z >0) � True ⦂ InstructionUnit□execute[positiveAddress],
	False ⦂ InstructionUnit□execute[elseAddress] ⍰) ⍰ §▮
	The formal syntactic definition of one-way named-message and receiving is Interface MetaaType has in the following end note: 73 ⟦history⟧ ↦ [RequestaType ⊛ ],
	reset[anActor:aType] ↦ Void▮
	Interface RequestaType has
	⟦message⟧ ↦ MessageaType ,
	⟦customer⟧ ↦ CustomeraType,
	⟦response⟧ ↦ FutureResponseanotherType▮
	Discrimination ResponseaType between
	ReturnedanotherType,
	Threw▮
	i VariableLocationaType has store[aType]↦ Void▮
	ii TemporaryLocationaType has write[aType] ↦ ⊝▮

// uses implementations // using this Actor with Human interface For example,

 Boy[Meter[3], Year[4]]∎⟦magnitude⟧▮ is equivalent to Meter[3]▮  Boy[Meter[3], Year[4]]∎ ⟦length⟧▮ is equivalent to Year[4]▮

Meta

Meta provides ability to provide extraordinary access to an Actor. For example, history of an Actor can be queried.

  The tokens ( and ) are used to delimit program syntax.The algorithm used in the implementation of CheeseQ above is due to Blaine Garst [private communication] cf.[Ladan-Mozes and Shavit 2004].

	ExpressionaType extends Construct with eval[Environment]↦ aType, perform[Environment, CheeseQ]↦ aType▮ BasicExpressionaType is an implementation that performs the functionality of leaving the cheese for expression being used as the continuation: Actor BasicExpressionaType[ ] perform[e:Environment, c:CheeseQ] → Try (anActor ← ⍠ExpressionaType∎eval[e] c∎release[ ] ⫼ anActor) cleanup c∎release[ ] §▮ Actor (anIdentifier:IdentifieraType):Expression aType:Type uses BasicExpressionaType[ ] | partially implements ExpressionaType using eval[e:Environment]:aType → e∎lookup[anIdentifier ]▮ The interface Type Interface thisType:: with extension?[_] ] |••> Boolean, has?[MethodSignature] |••> Boolean, sendOneWay[thisType, Message ↦⊝] ↦ ⊝, sendRequest[thisType, Message ↦aReturnType] ↦ aReturnType, encrypt[_] ↦ Encrypted, encrypterType[Type ] ↦ EncrypterType i , decrypt[Encrypted] ↦ thisType, decrypterType[thisType, EncrypterType] ↦ DecryptType ii , decrypt?[Encrypted] ↦ Boolean, return[CustomeraReturnType, aReturnType] ↦ Void, throw[Customer, Exception] ↦ Void▮ CommunicationType is a restriction that can be used only for communication: Interface thisType:CommunicationType restricts Type with sendOneWay[thisType, Message ↦⊝] ↦ ⊝, sendRequest[thisType, Message ↦aReturnType] ↦ aReturnType, return[CustomeraReturnType, aReturnType] ↦ Void, throw[Customer, Exception] ↦ Void▮ SendingType is a restriction of CommunicationType that can be used only for sending: Interface thisType:SendingType restricts CommunicationType with sendOneWay[thisType, Message ↦⊝] ↦ ⊝, sendRequest[thisType, Message ↦aReturnType] ↦ aReturnType▮ 79 Only an Actor that possesses dt2 can decrypt an Actor address encrypted using et2. Type Discrimination Interface DiscriminationType extends Type with up[Type] ↦ Discrimination, down[Discrimination] ↦ Type, down?[Discrimination] ↦ Boolean▮ Actor (anotherType:TypeanotherType "⊒?" aType:TypeaType):Expression Boolean uses BasicExpressionaType[ ] | partially implements ExpressionBoolean using eval[e:Environment]:Boolean → (anotherType ∎eval[e])∎extension?[aType∎eval[e]]▮ Actor (anExpression:Expression aType:Type "↑" castExpression:Type aDiscriminationType:Discrimination) :DiscriminationUp aType, aDiscriminationType uses BasicExpressionaType[ ] | partially implements ExpressionaType using eval[e:Environment]:aType → castExpression∎eval[e]∎up[anExpression∎eval[e]]▮ Actor (aPattern:Pattern aDiscriminationType "↑" castExpression:Type aDiscriminationType) :DiscriminationPatternUp aType, aDiscriminationType uses BasicPatternaDiscriminationType [ ] | partially implements PatternaDiscriminationType using match[anActor:DiscriminationInstanceaType, aDiscriminationType, e:Environment]:aType → aPattern∎match[aDiscriminationType∎up[anActor], e]▮ Actor (anExpression:Expression DiscriminationInstanceaType, aDiscriminationType "↓" castExpression:Type aType) :DiscriminationDown aType, aDiscriminationType uses BasicExpressionaType[ ] | partially implements ExpressionaType using eval[e:Environment]:aType → castExpression∎eval[e]∎down[anExpression∎eval[e]]▮ Actor (aPattern:Pattern aType "↓" castExpression:Type aType) :DiscriminationPatternDown aType, aDiscriminationType uses BasicPatternaType[ ] | partially implements PatternaType using match[anActor:DiscriminationInstanceaType, aDiscriminationType, e:Environment]:NullableEnvironment→ aPattern∎match[aDiscrminationType∎down[anActor], e]▮ Actor ("⋒⋒↓" aStructurePattern:Pattern aStructureType) :DownPatternaStructureType, aDiscriminationType uses BasicPatternaStructureType[ ] | partially implements PatternaStructureType using match[anActor:DiscriminationStructureInstanceaType, aDiscriminationType, e:Environment]:NullableEnvironment → structurePattern∎match[aDiscrminationStructureInstanceType ∎down?[anActor, aStructureType], e] � True ⦂ structurePattern∎match[aDiscrminationStructureInstanceType ∎down[anActor, aStructureType] e] False ⦂ Null Environment)▮ Actor ( aDiscrminationStructureInstanceType "⋒↓" aStructurePattern:Pattern aStructureType) :TypeDownPatternaStructureType, aDiscriminationType uses BasicPatternaStructureType[ ] | partially implements PatternaStructureType using match[anActor:DiscriminationStructureInstanceaType, aDiscriminationType, e:Environment]:NullableEnvironment → structurePattern∎match[aDiscrminationStructureInstanceType ∎down?[anActor, aStructureType], e] � True ⦂ structurePattern∎match[aDiscrminationStructureInstanceType ∎down[anActor, aStructureType], e] False ⦂ Null Environment)▮ Actor (anExpression:Expression DiscriminationInstanceaType, aDiscriminationType "↓?" castExpression:Type aType) :DiscriminationDownQueryaType, aDiscriminationType uses BasicExpressionBoolean[ ] | partially implements ExpressionBoolean using eval[e:Environment]:Boolean → aDiscriminationType∎down?[anExpression∎eval[e]]▮ Actor ("Discrimination" aDiscriminationType "between" typeExpressions:Types "▮"):Definition Actor implements Definition using eval[e:Environment]:Environment → (types ← typeExpressions∎eval[e], e∎bind[aDiscriminationType, type ⌸ DiscriminationType, to ⌸ Actor partially implements DiscriminationType with up[anInstance:aType∈types]:aDiscriminationType → SimpleDiscriminationInstance aType, aDiscriminationType[anInstance] ¶ down[anUpped :DiscriminationInstance aType, aDiscriminationType]:aType∈types → anUpped � ⋒⋒↓SimpleDiscriminationInstanceaType[anInstance] ⦂ anInstance ⍰ else ⦂ Throw CastException[ ], down?[anUpped:DiscriminationInstance aType, aDiscriminationType]:Boolean → anUpped � ⋒⋒↓SimpleDiscriminationInstanceaType[_] ⦂ True, else ⦂ False ⍰)▮ Structure SimpleDiscriminationInstanceaType, aDiscriminationType [anInstance:aType] extends DiscriminationInstanceaType, aDiscriminationType▮ Type restriction Interface RestrictionTypeaType extends Type with up[aType] ↦ RestrictionTypeaType▮ Actor (anExpression:Expression aType "↑" castExpression:Type RestrictionTypeaType) :RestrictionUp aType uses BasicExpressionaType[ ] | partially implements ExpressionRestrictionTypeaType using eval[e:Environment]:RestrictionTypeaType→ castExpression∎eval[e]∎up[anExpression∎eval[e]]▮ Actor ("Interface" aRestrictionType "restricts" typeExpression:Type aType "with" signatureExpressions:Signatures "▮"):Definition Actor implements Definition using eval[e:Environment]:Environment → (signatures ← signatureExpressions∎eval[e] typeExpression∎eval[e]∎has?[signatures] precondition e∎bind[aRestrictionType, type ⌸ RestrictionTypeaType, to ⌸ Actor implements RestrictionTypeaType using up[anInstance:aType]:aRestrictionType → RestrictionInstance[anInstance]])▮ Structure RestrictionInstance[anInstance:aType] uses BasicType[ ] | partially reimplements RestrictionTypeaType having (aMessage↦aReturnType)∈signatures) using sendRequest[aRecipient:aRestrictionType, aMessage:aMessage]:aReturnType → aRecipient � ⋒⋒↓RestrictionInstance[anInstance] ⦂ sendRequest[anInstance, aMessage], else ⦂ Throw CastException[ ]⍰ sendOneWay[aRecipient:aRestrictionType, aMessage:aMessage]:⊝ → aRecipient � ⋒⋒↓RestrictionInstance[anInstance] ⦂ sendOneWay[anInstance, aMessage], else ⦂ Throw CastException[ ]⍰▮ Type extension Interface ExtensionaType extends Type with up[ExtensionInstanceaType] ↦ aType, down[aType] ↦ ExtensionaType, down?[aType] ↦ Boolean▮ Actor (anExpression:Expression anExtensionType "↑" castExpression:Type aBaseType) :ExpressionUp anExtensionType, aBaseType uses BasicExpressionaBaseType[ ] | partially implements ExpressionaBaseType using eval[e:Environment]:aBaseType → castExpression∎eval[e]∎up[anExpression∎eval[e]]▮ Actor (aPattern:Pattern anExtensionType "⋒↑" castExpression:Type anExtensionType) :PatternUp anExtensionType, aBaseType uses BasicPatternanExtensionType[ ] | partially implements PatternanExtensionType using match[anActor:ExtensionInstanceanExtensionType, aBaseType, e:Environment]:aType → aPattern∎match[anExtensionType∎up[anActor], e]▮ Actor (anExpression:Expression aBaseType "↓" castExpression:Type anExtensionType) :ExtensionDown anExtensionType, aBaseType uses BasicExpressionanExtensionType[ ] | partially implements ExpressionanExtensionType using eval[e:Environment]:aType → castExpression ∎eval[e]∎down[anExpression ∎eval[e]]▮ Actor (aPattern:Pattern anExtensionType "⋒↓" castExpression:Type anExtensionType) :ExtensionPatternDown aBaseType, anExtensionType uses BasicPatternaBaseType[ ] | partially implements PatternaBaseType using match[anActor:ExtensionInstanceaBaseType, anExtensionType, e:Environment]:NullableEnvironment → aPattern∎match[castExpression∎eval[e]∎down[anActor], e]▮ Actor (anExpression:Expression aBaseType "↓?" castExpression:Type anExtensionType) :ExpressionDownQuery anExtensionType, aBaseType uses BasicExpressionBoolean[ ] | partially implements ExpressionBoolean using eval[e:Environment]:aType → castExpression ∎eval[e]∎down?[anExpression ∎eval[e]]▮ Actor ("Actor" anExtensionType "extends" Type aType "▮") :Definition Actor implements Definition using eval[e:Environment]:Environment → e∎bind[anExtensionType, type ⌸ RestrictionTypeaType, to ⌸ Actor uses BasicType[ ] | partially implements ExtensionaType using up[anInstance:anExtensionType]:aType → ExtensionInstanceaType[anInstance] ¶ down[anUpped:aType]:anExtensionType→ anUpped � ⋒⋒↓ExtensionInstanceanExtensionType, aType [anInstance] ⦂ anInstance, else Throw CastException[ ]⍰ ¶ down?[anUpped:aType]:Boolean → anUpped � ⋒⋒↓ExtensionInstanceanExtensionType, aType [_] ⦂ True, else False⍰ §▮ Structure ExtensionInstanceanExtension, aType [anInstance:anExtension] extends aType▮ Nullable, e.g., • The type Nullable is used for nullables: Implementation NullableaType has reduce?[ ]↦ Boolean, reduce[ ]↦ aType▮ Actor ("Nullable" anExpression:Expression aType) :Nullable aType uses BasicExpressionNullableaType[ ] | partially implements ExpressionNullableaType using eval[e:Environment]:NullableaType→ (anActor ← anExpression∎eval[e] Actor implements NullableaTypeusing reduce?[ ]:Boolean → True ¶ reduce[ ]:aType → anActor §)▮ Actor (Null aType:Type aType):NullExpression aType uses BasicExpressionNullableaType[ ] | partially implements ExpressionNullableaType using eval[e:Environment]:NullableaType → Actor implements NullableaType using reduce?[ ]:Boolean → False ¶ reduce[ ]:aType → Throw IsNullException[ ] §▮ Actor (TheNull):NullPattern aType implements PatternNullableaType using match[anActor:NullableaType, e:Environment] :NullableEnvironment → anActor � TheNull ⦂ Nullable e, else ⦂ Null Environment ⍰ §▮ Actor ("•" anExpression:Expression NullableaType) :Expression aType uses BasicExpressionaType[ ] | partially implements ExpressionaType using eval[e:Environment]:aType → (anExpression∎eval[e]∎reduce[ ] §▮ Future, e.g., •, and ℗ The type Future is used for futures: Implementation FutureaType has reduce[ ]↦ aType▮ Actor ("⋒•" aPattern:Pattern NullableaType) :Pattern aType implements PatternNullableaType using match[anActor:NullableaType, e:Environment] :NullableEnvironment → anActor∎reduce?[ ] � True ⦂ aPattern∎match[anActor ∎reduce[ ], e] � TheNull ⦂ Nullable e, else ⦂ Null Environment ⍰, False⦂ Null Environment ⍰ §▮ Actor ("Future" anExpression:Expression aType) :Future aType uses BasicExpressionFutureaType[ ] | partially implements ExpressionFutureaType using eval[e:Environment]:FutureaType → (aFuture ← Future Try anExpression∎eval[e] catch� anException ⦂ Actor implements FutureaType using reduce[ ]:aType → Throw anException §⍰ Actor implements FutureaTypeusing reduce[ ]:aType → •aFuture §)▮ Actor ("•" anExpression:Expression FutureaType) :Reduction aType uses BasicExpressionaType[ ] | partially implements ExpressionaType using eval[e:Environment]:aType → empty?[ ] ↦ Boolean▮ anExpression∎eval[e]∎reduce[ ] §▮ The message match Patterns are analogous to expressions, except that they have receive match messages: Interface PatternaType with match [aType, Environment]↦ NullableEnvironment▮ Actor ("⋒•" aPattern:PatternFutureaType) :Pattern aType implements PatternFutureaType using match[anActor:FutureaType, e:Environment] :NullableEnvironment → aPattern∎match[anActor ∎reduce[ ], e] � TheNull ⦂ Nullable e, else ⦂ Null Environment ⍰, §▮ Actor ("℗" anExpression:Expression aType) :Mandatory aType uses BasicExpressionaType[ ] | implements ExpressionaType using eval[e:Environment]:aType → •Future anExpression∎eval[e] §▮ Actor (anIdentifier:Identifier aType):Pattern aType implements PatternaType using match[anActor:aType, e:Environment]:NullableEnvironment → e∎bind[anIdentifier, type ⌸ aType, to ⌸ anActor]▮ Actor ("_"):UniversalPattern aType implements PatternaType using match[anActor:aType, e:Environment]:NullableEnvironment → Nullable e▮ Message sending, e.g., ∎ Actor ("⌕" anExpression:Expression aType) :ValuePattern aType implements PatternaType using match[anActor, e:Environment]:NullableEnvironment → anActor � anExpression∎eval[e] ⦂ Nullable e, else ⦂ Null Environment ⍰▮ Actor (procedure:Expression argumentsType↦returnType "∎" "[" arguments:Arguments argumentsType "]") :ProcedureSend returnType uses BasicExpressionreturnType[ ] | partially implements ExpressionreturnType using eval[e:Environment]:returnType → (procedure∎eval[e])∎[⩛(expressions∎eval[e])] §▮ Actor (recipient:Expression recipientType "∎" name:MessageName "[" arguments:Arguments argumentsType "]") :NamedMessageSend returnType uses BasicExpressionreturnType[ ] | partially implements ExpressionreturnType using eval[e:Environment]:returnType → (aRecipient ← recipient∎eval[e], aRecipient∎SimpleMessage[QualifiedName[name, recipientType], [⩛arguments∎eval[e]]] §▮ Actor (recipient:Expression recipientType "∎" aMessage:Message messageType) :UnnamedMessageSend returnType uses BasicExpressionreturnType[ ] | partially implements ExpressionreturnType using eval[e:Environment]:returnType → recipientType∎send[recipient∎eval[e], aMessage∎eval[e]] §▮ Exceptions Continuations using perform A continuations is a generalization of expression for executing in cheese, which receives perform messages: Interface ContinuationaType extends Construct with perform[Environment, CheeseQ]↦ aType▮ Actor ("Try" anExpression:Expression aType "catch�" exceptions:ExpressionCases Exception, aType "⍰") :TryExpression aType uses BasicExpressionaType[ ] | partially implements ExpressionaType using eval[e:Environment]:aType → Try anExpression∎eval[e] catch� anException:Exception ⦂ CasesEval∎[anException, exceptions, e] ⍰ §▮ Actor ("Try" anExpression:Expression aType "cleanup" aCleanup:Expression aType) :TryExpression aType uses BasicExpressionaType[ ] | partially implements ExpressionaType using eval[e:Environment]:aType → Try anExpression∎eval[e] catch� _ ⦂ (aCleanup∎eval[e] Rethrow)⍰ §▮ Actor ExecuteaType [aConstruct:Construct, e:Environment, c:CheeseQ]:aType → aConstruct � aContinuation↓ContinuationaType ⦂ aContinuaton∎perform[e, c], anExpression↓ExpressionaType ⦂ anExpression∎eval[e] ⍰▮ Actor (anExpression:Expression anotherType "�" cases:ContinuationCases anotherType, aType "⍰") :CasesContinuation aType implements ContinuationaType using perform[e:Environment, c:CheeseQ]:aType → CasesPerform∎[anExpression∎eval[e], cases, e, c] §▮ Actor CasesPerform [anActor:anotherType, cases:[ContinuationCaseaType ⊛ ], e:Environment, c:CheeseQ]:aType → cases � [ ] ⦂ Throw NoApplicableCase[ ], [first, ⩛rest] ⦂ first � (aPattern:Pattern anotherType"⦂" aContinuation:Continuation aType) :ContinuationCase aType ⦂ aPattern∎match[anActor, e] � TheNull ⦂ CasesPerform∎[anActor, rest, e, c], ⋒•newEnvironment ⦂ aContinuation∎perform[newEnvironment, c] ⍰, ("else" elsePattern:Pattern anotherType "⦂" elseContinuation:Continuation aType) :ContinuationElseCase aType ⦂ elsePattern∎match[anActor, e] � TheNull ⦂ Throw ElsePatternMustMatch[ ], ⋒•newEnvironment ⦂ elseContinuation∎eval[newEnvironment] ⍰, ("else" "⦂" elseContinuation:Continuation aType) :ContinuationElseCase aType ⦂ elseContinuation∎perform[e, c], else ⦂ Throw NoApplicableCase[ ] ⍰⍰▮ Holes in the cheese Actor (anExpression:Expression aType "↺" someAssignments:Assignments ) :Afterward aType implements ContinuationaType using perform[e:Environment, c:CheeseQ]:aType → (anActor ← anExpression∎eval[e] someAssignments∎carryOut[e, c] c∎release[ ] anActor) §▮ Actor (aVariable:Variable aType "≔" anExpression:Expression aType):Assignment implements Assignment using carryOut[e:Environment]:Void → e∎assign[aVariable, to ⌸ anEpression∎eval[e]] §▮ Actor ("Hole" anExpression:Expression aType):Hole aType implements ContinuationaType using perform[e:Environment, c:CheeseQ]:aType → (frozenEnvironment ← e∎freeze[ ] // create frozen environment so that subsequent assignments // subsequent assignments do not affect evaluating anExpression c∎release[ ] anExpression∎eval[frozenEnvironment) §▮ Actor ("(" aPreparations:Preparations anExpression:Expression aType")") :CompoundExpression aType implements ContinuationaType using perform[e:Environment, c:CheeseQ]:aType → (frozenEnvironment ← e∎freeze[ ] // create frozen environment so that // preparation does not affect evaluating anExpression aPreparation∎carryOut[e, c] c∎release[ ] anExpression∎eval[frozenEnvironment]) §▮ Actor ("Hole" anExpression:Expression anotherType "↺" anAfterward:AfterwardContinuation aType "⍰") :Hole aType implements ContinuationaType using perform[e:Environment, c:CheeseQ]:aType → (frozenEnvironment ← e∎freeze[ ] c∎release[ ] Try (anActor ← anExpression∎eval[frozenEnvironment] Holding c in anAfterward∎perform[e, c]] anActor) catch� _ ⦂ (Holding c in anAfterward∎perform[e, c] Rethrow)⍰ §▮ Actor ("Holding" resourceExpression:Expression Resource "in" anExpression Expression aType "⍰") :HoldingExpression aType uses BasicExpressionaType | partially implements ExpressionaType using eval[e:Environment]:aType → (resource ← resourceExpression ∎eval[e], resource∎acquire[ ] Try (anActor ← anExpression ∎eval[e], resource∎release[ ], anActor) catch� _ ⦂ (resource∎release[ ] Rethrow)⍰ §▮ ("Hole" anExpression:Expression anotherType "returned�" returnedCases:ContinuationCases anotherType, aType "⍰" "threw�" threwCases:ContinuationCases anotherType, aType "⍰") :HoleanotherType, aType perform[e:Environment, c:CheeseQ]:aType → (frozenEnvironment ← e∎freeze[ ] c∎release[ ] Try (anActor ← anExpression∎eval[frozenEnvironment] c∎acquire[ ] CasesPerform∎[anActor, returnedCases, e, c]) cleanup (c∎acquire[ ] CasesPerform∎[anException, threwCases, e, c])⍰ §▮ Actor ("Enqueue" anExpression:QueueExpression ""):Enqueue implements Continuation using perform[e:Environment, c:CheeseQ]:Void → anExpression∎eval[e]∎enqueueAndLeave[ ] §▮ Actor InitializedaType [anInterface:aType, handlers:[Handler ⊛ ], e:Environment, c:CheeseQ]:aType → Actor implements anInterface using receivedMessage:TypeMessage → // receivedMessage received for anInterface (c∎acquire[ ] aReturned ← Try Select∎[receivedMessage, handlers, e, c] cleanup c∎release[ ] // release cheese and rethrow exception c∎release[ ] aReturned) §▮ The implementation CheeseQ uses activities to implement its queue where Implementation Activity has ⟦previous⟧ ↦ NullableActivity // returns self so that updates can be chained ⟦nextHint⟧ ↦ NullableActivity // if non-null then pointer to next activity to get cheese after this one ⟦nextHint ≔ NullableActivity⟧ ↦ NullableActivity▮ // returns self so that updates can be chained Implementation type InternalQ is defined on the next page where: Implementation InternalQ has enqueueAndLeave[ ] ↦ Void, enqueueAndDequeue[InternalQ] ↦ Activity dequeue[ ] ↦ Activity ← � ?? cases separator ⍰ ⍰ ??? end cases terminator � and catch� ¶ \p 92 another message handler separator for § \s end handlers terminator implements and extension ⦂ (:) case separator for case  ; before separator binding, preparation ⫼ ||| concurrently separator binding, /* /* begin comment prefix */ and Enqueue comment preparation // // begin 1-line prefix EndOfLine 2BC3 infix ⊩ ||-goal prefix and 22A9 2982 infix ⊢ |-assert prefix and 22A2 00A7  -| logical negation prefix 00D8 handlers → disjunction 00B6  \/ logical infix 00DA 2370 conjunction FFFD  /\ logical infix 00D9 <--be 91 infix 2190 equivalence ⟦previous ≔ NullableActivity⟧ ↦ NullableActivity ↠ pair infix 21A0 ⇔  logical infix 21D4 // if null then head of queue else, pointer to backwards list to head concurrent ↦ |-> message type |••> |..> → --> message received 90 infix λ and/or ¶ implication 2192 ⇒  logical infix 21E8 cacheable ↦ ⊒  extends infix 2292 returns type 89 infix ⊑  constrained by infix 2291 21A6 ⊔ |_| join infix 2294 ℗ \P 88 necessarily prefix 29B7 □ \ one-way send infix 219E implements ContinuationaType using Simple Implementation of Actor The implementation below does not implement queues, holes, and relaying. Actor ("Enqueue" anExpression:QueueExpression "" aContinuation:Continuation aType):Enqueue aType implements ContinuationaType using perform[e:Environment, c:CheeseQ]:aType → (anInternalQ ← anExpression∎eval[e], anInternalQ∎enqueueAndLeave[ ] aContinuation∎perform[e, c]) §▮ Actor ("Actor" declarations:ActorDeclarations "implements" IdentifieraType "using" handlers:Handlers anInterface " §"):Definition implements ExpressionanInterface using eval[e:Environment]:aType → InitializedaType∎[anInterface∎eval[e], handlers, declarations∎initialize[e], CheeseQ∎[ ]] §▮ and Enqueue ⇔, 85 Actor Select [receivedMessage:Message, handlers:[Handler ⊛ ], e:Environment, c:CheeseQ]:aType → handlers � [ ] ⦂ Throw MessageRejected[ ], [(aMessageDeclaration:MessageDeclaration aType ":" ReturnDeclaration aType "→" body:Continuation aType) :ContinuationHandleraType, aMessageDeclaration∎match[receivedMessage, e] � TheNull ⦂ // process next handler ⋒•newEnvironment ⦂ ExecuteaType∎[body, newEnvironment, c] ⍰⍰▮ // execute body with augmentation of e As a consequence of the definition of CheeseQ: Implementation CheeseQ has acquire[ ] ↦ Void release[ ] ↦ Void▮ aTail != NullTask enter[ ] ⟐↑ ~^ match upped prefix ⨀ (.) qualified by infix λ /\ procedure prefix ≡ and/or → ≡ === defined as infix Define ∎ is sent infix ∎∎ .. send to this Actor prefix ⊝ (-) nothing 96 expression 229D 2025 ⋮ ::: uniformly of a type infix 22EE . ⊛ (*) zero or more postfix 229B 2261 ( (| begin syntax left delimiter 2985 03BB ( ( begin grouping left delimiter ) 22A1 " \" Left string structure left delimiter " 201C aHeadHint = aTail ↑ ^^ up infix 2191 message Select∎[receivedMessage, restHandlers, e, c], 1 in thisCheeseQ > 1 in thisCheeseQ aTail != NullTask 1 left ⟐↓ ~\v/ match downed ⟦ [| formatted left delimiter ⟧ 27E6 infix aHeadHint != aTail ↓? \v/? down query infix ⦃ {| begin multi-set left delimiter ⦄ 2983 leave[ ] ↓ \v/ down infix 2193 [ [ begin list left delimiter ] ⩛restHandlers] ⦂ There is a state diagram for the implementation below: 0 in thisCheeseQ aTail = NullTask aHeadHint = NullTask enter[ ] leave[ ] enter[ ] > 1 left (hex) ▮ ;; end top level : : of specified type :: :: is a type ⍠ [:] this Actor with • \O 86 reduce ⟐• ~\O 87 match reduced (nullables, futures) { { begin set left delimiter } prefix ⩛ \|/ spread 95 prefix 2A5B (nullables, futures) prefix 29BE 0077) parameters (Unicode hex: interface (aspect) prefix  <| begin type left delimiter  0076 2360 :⌸ :[=] assignable field infix postfix ⌸ [=] keyword or field infix 2338 infix ≠ != Different from? infix 2260 terminator = = same as? infix 25AE of 94 ⌕ \o 93 matches value prefix 2315 Unicode ≔ := is assigned infix 2254 ↺ U^ afterward infix 21BA ↺
	i Interface Construct▮

i C# is a registered trademark of Microsoft, Inc.Java and JavaScript are registered trademarks of Oracle, Inc.Objective C is a registered trademark of Apple, Inc. ii with no single point of failure

i An implementation type cannot be downcast because there is nothing to which to downcast. Note that this means that an implementation type cannot be subtyped although an implementation can use other implementations for modularity. Of course, for interface types there is no semantic guarantee of what an implementation of the interface might do as long as it obeys the signatures.

iii The procedure P may be indeterminate, i.e., return different results on successive calls. iv The procedure P may be indeterminate, i.e., return different results on different calls.

i Implementation EncrypterType has encrypt[thisType] ↦ Encrypted▮ ii Implementation DecrypterType has decrypt[Encrypted] ↦ thisType, decrypt?[Encrypted] ↦ Boolean▮

i These are only examples. They can be redefined using keyboard macros according to personal preference.

Acknowledgements

Important contributions to the semantics of Actors have been made by: Gul Agha, Beppe Attardi, Henry Baker, Will Clinger, Irene Greif, Carl Manning, Ian Mason, Ugo Montanari, Maria Simi, Scott Smith, Carolyn Talcott, Prasanna Thati, and Aki Yonezawa. Alan Kay. "Personal Computing" in Meeting on 20 Years of Computing Science Instituto di Elaborazione della Informazione, Pisa, Italy. 1975. http://www.mprove.de/diplom/gui/Kay75.pdf Frederick Knabe A Distributed Protocol for Channel-Based Communication with Choice PARLE'92. Bill Kornfeld and Carl Hewitt. The Scientific Community Metaphor IEEE Transactions on Systems, Man, and Cybernetics. January 1981. Bill Kornfeld. Parallelism in Problem Solving MIT EECS Doctoral Dissertation. August 1981. Robert Kowalski. A proof procedure using connection graphs JACM. October 1975. Robert Kowalski Algorithm = Logic + Control CACM. July 1979. Robert Kowalski. Response to questionnaire Special Issue on Knowledge Representation. SIGART Newsletter. February 1980. Robert Kowalski (1988a) The Early Years of Logic Programming CACM. January 1988. Robert Kowalski (1988b) Logic-based Open Systems Representation and Reasoning. Stuttgart Conference Workshop on Discourse Representation, Dialogue tableaux and Logic Programming. 1988. Edya Ladan-Mozes and Nir Shavit. An Optimistic Approach to Lock-Free FIFO Queues Distributed Computing. Sprinter. 2004. Leslie Lamport How to make a multiprocessor computer that correctly executes multiprocess programs IEEE Transactions on Computers. 1979. Peter Landin. A Generalization of Jumps and Labels UNIVAC Systems Programming Research Report. August 1965. (Reprinted in Higher Order and Symbolic Computation. 1998) Peter Landin A correspondence between ALGOL 60 and Church's lambda notation CACM. August 1965. Edward Lee and Stephen Neuendorffer Classes and Subclasses in Actor-Oriented Design. Conference on Formal Methods and Models for Codesign (MEMOCODE). June 2004. Steven Levy Hackers: Heroes of the Computer Revolution Doubleday. 1984. Henry Lieberman. An Object-Oriented Simulator for the Apiary Conference of the American Association for Artificial Intelligence, Washington, D. C., August 1983 Henry Lieberman. Thinking About Lots of Things at Once without Getting Confused: Parallelism in Act 1 MIT AI memo 626. May 1981. Henry Lieberman. A Preview of Act 1 MIT AI memo 625. June 1981. Henry Lieberman and Carl Hewitt. A real Time Garbage Collector Based on the Lifetimes of Objects CACM June 1983. Barbara Liskov and Liuba Shrira Promises: Linguistic Support for Efficient Asynchronous Procedure Calls SIGPLAN'88. Barbara Liskov and Jeannette Wing . A behavioral notion of subtyping, TOPLAS, November 1994.

Enumerations, i.e., Enumeration of using Qualifiers, i.e., ` An enumeration definition provides symbolic names for alternatives using "Enumeration" followed by the name of the enumeration, "of", a list of distinct identifiers terminated by "▮".

For example, Enumeration DayName of Monday, Tuesday, Wednesday, Thursday, Friday, Saturday, Sunday▮

From the above definition, an enumerated day is available using a qualifier, e.g., Monday⨀DayName. Qualifiers provide for namespaces.

The formal syntax of qualifiers is in the following end note: 69.

The procedure below computes the name of following day of the week given the name of any day of the week:

UsingNamespace DayName▮ Define FollowingDay[aDay:DayName]:DayName ≡ aDay � Monday ⦂ Tuesday, Tuesday ⦂ Wednesday, Wednesday ⦂ Thursday, Thursday ⦂ Friday, Friday ⦂ Saturday, Saturday ⦂ Sunday, Sunday ⦂ Monday ⍰▮

The formal syntax of enumerations is in the following end note: 70.

Native types, e.g., JavaScript, JSON, Java, HTML (HTTP), and XML Because Actor addresses are typed, almost any kind of addressed can be accommodated.

Object can be used to create JavaScript Objects. Also, Function can be used to bind the reserved identifier This. For example, consider the following ActorScript for creating a JavaScript object aRectangle (with length 3 and width 4) and then computing its area 12: (aRectangle i ← Object {"length": 3, "width": 4]}, aFunction ← Function [ ]→ This⟦"length"⟧  This⟦"width"⟧, Rectangle⟦"area"⟧ ≔ aFunction aRectangle⟦"area"⟧∎[ ])▮

i aRectangle is of type Object`JavaScript

The setTimeout JavaScript object can be invoked with a callback as follows that logs the string "later" after a time out of 1000: setTimeout⨀JavaScript∎[1000, Function [ ]→ console⨀JavaScript∎["log"]∎["later"]]▮ HTML strings can be used to create Actor addresses. For example, the Wikipedia English homepage can be retrieved as follows: 71 (HTTPS["en.wikpedia.org"])∎get[ ] JSON is a restricted version of Object that allows only Booleans, numbers, strings in objects and arrays. i

Native types can also be used from Java. For example, if s:String⨀Java, then s∎substring [3,5] ii is the substring of s from the 3 rd to the 5 th characters inclusive.

Java types can be referenced using Refer iii , e.g.:

Refer java.math.BigInteger▮ Refer java.lang.Number▮

The following notation is used for XML: 72 XML <"PersonName"> <"First">"Ole-Johan" </"First"> <"Last"> "Dahl"</"Last"> </"PersonName"> and could print as: <PersonName> <First> Ole-Johan </First> <Last> Dahl </Last> </PersonName> XML Attributes are allowed so that the expression XML <"Country" "capital"="Paris"> "France" </"Country"> and could print as: <Country capital="Paris"> France </Country> i i.e. the following JavaScript types are not included in JSON: Date, Error, Regular Expression, and Function. ii substring is a method of the String type in Java iii Refer is called Import in Java One-way messaging, e.g., ⊝, and □ One-way messaging is often used in hardware implementations.

Each one-way named-message send consists of an expression followed by "□", a message name, and arguments delimited by "[" and "]".

Each one-way message handler implementation consists of a named-message declaration pattern, ":", "⊝", "→" and a body for the response which must ultimately be "⊝" which denotes no response.

XML construction can be performed in the following ways using the append operator:  XML <"doc"> 1, 2, ⩛[3] </"doc">]▮ is equivalent to XML <"doc">1, 2, 3</"doc">▮  XML <"doc">1, 2, ⩛[3], ⩛[4] </"doc">]▮ is equivalent to XML <"doc"> 1, 2, 3, 4 </"doc">▮

Inconsistency Robust Logic Programs

Logic Programs 75 can logically infer computational steps.

Forward Chaining

Forward chaining is performed using ⊢ Illustration of forward chaining:

⊢t

Backward Chaining

Backward chaining is performed using ⊩ ("⊢" Theory PropositionExpression )

Assert PropositionExpression for Theory.

("When" "⊢" Theory aProposition:Pattern "→" Expression )

When aProposition holds for Theory, evaluate Expression.

("⊩" Theory aGoal:Pattern "→" Expression )

Set aGoal for Theory and when established evaluate Expression.

("⊩" Theory aGoal:Pattern ):Expression Set aGoal for Theory and return a list of assertions that satisfy the goal.

("When" "⊩" Theory aGoal:Pattern "→" Expression )

When there is a goal that matches aGoal for Theory, evaluate Expression.

Aggregation using Ground-Complete Predicates

Logic Programs in ActorScript are a further development of Planner. For example, suppose there is a ground-complete predicate 76 Link[aNode, anotherNode, aCost] that is true exactly when there is a path from aNode to anotherNode with aCost.

When ⊩ Path[aNode, aNode, aCost]→ // when a goal is set for a cost between aNode and itself

⊢ aCost =0▮

// assert that the cost from a node to itself is 0

The following goal-driven Logic Program works forward from start to find the cost to finish : 77

Path[next, finish, remainingCost]}▮ // a cost from start to finish is the minimum of the set of the sum of the // cost for the next node after start and // the cost from that node to finish

The following goal-driven Logic Program works backward from finish to find the cost from start :

Path[start, previous, remainingCost]}▮ // the cost from start to finish is the minimum of the set of the sum of the // cost for the previous node before finish and // the cost from start to that Node Note that all of the above Logic Programs work together concurrently providing information to each other. It might seem that a meta-circular definition is a strange way to define a programming language. However, as shown in the references, concurrent programming languages are not reducible to logic. Consequently, an augmented meta-circular definition may be one of the best alternatives available.

The message eval

John McCarthy is justly famous for Lisp. One of the more remarkable aspects of Lisp was the definition of its interpreter (called Eval) in Lisp itself. The exact meaning of Eval defined in terms of itself has been somewhat mysterious since, on the face of it, the definition is circular. 78 The basic idea is to send an expression an eval message with an environment to instead of the Lisp approach of sending the procedure Eval the expression and environment as arguments.

Suppose there is a type Account that needs have accounts that can be shared selectively among some IoT devices so that i  some of the devices can operate using the address of an account  some can only pass on an inoperable opaque address of the account  some can convert an inoperable opaque address to an operable address of the account  and some can convert an operable account address to an opaque inoperable address.

Construct type et1 (that has the operations on accounts) using the constructor

An implementation of cheese that never holds a lock

The following is an implementation of cheese that does not hold a lock: " and the character " to delimit tokens. For example, (3 "+" 4) is an expression that can be evaluated to 7. A special font is used for syntactic categories. For example, (x:Numerical "+" y:Numerical ):Numerical ▮ Numerical ⊑Expression ▮ Also, (Numerical "-" Numerical ):Numerical ▮ ("-" Numerical ):Numerical ▮ (Numerical "" Numerical ):Numerical ▮ (Numerical "" Numerical ):Numerical ▮ ("Remainder" Numerical "" Numerical ):remainder:Numerical ▮ ("QuotientRemainder" Numerical "" Numerical ) :[Numerical, Numerical ]▮ ("True" ⊔ "False" ):Expression ▮ (Expression "" Expression ):Expression ▮ (Expression "" Expression ):Expression ▮ ( "" Expression ):Expression ▮ ( "Throw" Expression ):Expression ▮ 4 See explanation of syntactic categories above. A word must begin with an alphabetic character and may be followed by one or more numbers and alphabetic characters.

Identifier ⊑Word ⊑Expression ▮ // an Identifier is a Word, which is a subcategory of Expression ((Expression ⊔ Definition ⊔ Judgment )) "▮"):Top▮ 5 (Identifier ":" Type ):Declaration // Identifier is declared to be of Type (Identifier "::" ):Declaration // Identifier is declared to be a type (Type "↦" Type ):Signature ▮ (Type "↦" "⊝") :Signature ▮ ("[" Types "]"):Type ▮ ( ⊔ MoreTypes ):Types ▮ (Type ⊔ (Type ","MoreTypes )):MoreTypes ▮ 6 (Identifier "←" Expression ):Definition ▮ (Preparation ("," ⊔ "") MorePreperations )):Preparations ▮ (Expression ):MorePreperations ▮ 7 Generalization of the notation of [START_REF] Church | A Set of postulates for the foundation of logic (1&2)[END_REF]]. 8 ("Define" ProcedureName "∎" "[" ArgumentDeclarations "]" ":" Type "≡" :MoreComponentPatterns ▮

19 [START_REF] Dijkstra | Go To Statement Considered Harmful Letter to Editor CACM[END_REF] famously blamed the use of the goto as a cause and symptom of poorly structure programs. However, assignments are the source of much more serious problems. 20 Continuations in ActorScript are related to continuations introduced in [START_REF] Reynolds | Definitional interpreters for higher order programming languages[END_REF]] in that they represent a continuation of a computation. The difference is that a continuation of Reynolds is a procedure that has as an argument the result of the preceding computation. Consequently, a continuation of Reynolds is closer to a customer in the Actor Model of computation. 21 ("Actor" :MoreInterfaceImplementations ▮ (( ⊔ "partially") ("implements" ⊔ "reimplements") ( ⊔ "exportable") Type "using" (MessageHandlers " §")⊔ UniversalMessageHandler :MoreContinuationElseCases ▮ (("else" "⦂" ContinuationList ) ⊔ ("else" Pattern "⦂"ExpressionsContinuation ))

:ContinuationElseCase ▮ // The else case is executed only if the patterns before // the else case do not match the value of test.

(Pattern "⦂" ExpressionsContinuation ):ContinuationCase ▮

The following are allowed in the cheese for a response to message affecting the next message: (Expression ( ⊔ ( "permit" aQueue:Expression )) ( ⊔ ("↺" Afterward ))):Continuation ▮ /* If there are activities in aQueue, then the one of them gets the cheese next and also perform Afterward, then release the cheese and return the value of Expression . /* VariableAssignments :Afterward ▮ ("Permit" aQueue:Expression ( ⊔ ("also" VariableAssignments))):PermitAlso ▮

The following can be used temporarily release the cheese:

("Hole" Expression ):Continuation  The records are cacheable because their type is {ContactRecord ⊛ }  All of the operators are cacheable  The operators are annotated as cacheable using "|••>" 57 ("Encrypt" Expression):Expression Define ("Encrypt" anExpression:Expression ) ≡ (aType "∎ " "encrypt" "[" anExpression "]") 58 It is possible to define a procedure that will produce a "bottomless" future.

For "→"ExpressionsContinuation ):MessageHandler ▮ /* one-way message handler implementation with ArgumentDeclarations that has a one-way continuation that returns nothing */ ("⊝" ( ⊔ ( "permit" aQueue:Expression )) ( ⊔ ("↺" Afterward ))):Continuation ▮ 74 note the absence of "∎" in the implementation subexpressions.

Male[aMagnitude] is invoked concurrently with Human[aLength].

108 75 [START_REF] Church | A Set of postulates for the foundation of logic (1&2)[END_REF][START_REF] Mccarthy | Situations, actions and causal laws Technical Report Memo[END_REF]Hewitt 1969Hewitt , 1971Hewitt , 2010;;[START_REF] Milner | Logic for Computable Functions: description of a machine implementation[END_REF], Hayes 1973;Kowalski 1973]. Note that this definition of Logic Programs does not follow the proposal in [Kowalski 1973[Kowalski , 2011] that Logic Programs be restricted only to programs. 76 A ground-complete predicate is one for which all instances in which the predicate holds are explicitly manifest, i.e., instances can be generated using patterns. See [Ross andSagiv 1992, Eisner and[START_REF] Eisner | Dyna: Extending Datalog for modern AI[END_REF]. 77 Execution can proceed differently depending on how sets fit into computer storage units.

78 /* Consider a dialect of Lisp which has a simple conditional expression of the following form:

("(" "if " test:Expression then:Expression else:Expression ")" ) which returns the value of then if test evaluates to True and otherwise returns the value of else.