Padlock

Padlock is a thematic, Turing-complete process calculus based on the mathematical model of π-calculus, by User:RocketRace.

Syntax

Padlock programs consist of processes (denoted here with P or Q) and names (denoted here with x or y). Padlock programs are made up of six different characters based on Unicode emoji for locks, using a lisp-style prefix syntax. Alternate ASCII symbols may be used instead, for some text encodings.

Symbol	Alternate Symbol	Usage within programs	Effect
🔒	N	🔒	Nil process. Takes no arguments.
🔓	S	🔓PQ	"Split" instruction. Executes processes P and Q in parallel.
🔐	E	🔐x🖋y🖋P	"Send" instruction. Encrypts the name x and sends the encrypted name along channel y, then executes process P.
🔏	R	🔏x🖋y🖋P	"Receive" instruction. Receives a name on channel y and binds that name to x, then executes process P.
🔑	K	🔑x🖋y🖋P	"Decrypt" instruction. Takes name x, decrypts it once, binds the result to y, then executes process P in parallel with the whole instruction. That is, 🔑x🖋y🖋P is equivalent to 🔑x🖋y🖋🔓P🔑x🖋y🖋P
🖋	P	🖋x🖋P	"Name" instruction. Binds a name x, then executes process P.

The set of free names in a process P is defined inductively by the table below. The free names of a process P are names that are not bound in the process.

Process	Free names
🔒	None
🔓PQ	All free names of P and Q
🔐x🖋y🖋P	x; y; all free names of P
🔏x🖋y🖋P	x; all free names of P, except for y
🔑x🖋y🖋P	x; y; all free names of P
🖋x🖋P	All free names of P, except for x

Communication

All communication instructions, that is, 🔏 and 🔐, will only execute the next process in their chain once they successfully send or receive a name on some channel. This means that any attempt to send to / receive from the channel will pause the process until both a sender and a recipient are on the same channel simultaneously.

Encryption

Encryption and decryption are ideal and reversible. That is, only x_0 can be encrypted into x_1, and only x_1 can be decrypted into x_0. If names x and y are each encrypted or decrypted, never will x_n be equal to y_m, for some integers n and m representing the amount of times x and y have been encrypted / decrypted. Additionally, a name may be encrypted or decrypted an arbitrary amount of times. An unencrypted name x_0 may also be "decrypted" into x_-1.

Undefined behavior

Padlock contains necessarily undefined behavior, enumerated below.

1. When more than one process attempts to send a name to a channel, only one process will be successful, but the choice of process is undefined.
2. When more than one process attempts to receive a name from a channel, only one process will be successful, but the choice of process is undefined.

Computational class

π-calculus is capable of universal computation, being able to evaluate lambda calculus. π-calculus can be embedded in Padlock, from which follows that Padlock too is Turing-complete. The following table describes the substitutions necessary for this embedding. Here, the naming convention for processes and names presented above is used for both process calculi.

π-calculus syntax	Substitution in Padlock
0	🔒
P|Q	🔓PQ
(vx).P	🖋x🖋P
x_{y}.P	🔐y🖋x🖋P
x(y).P	🔏a🖋x🖋🖋b🖋🔓🔐b🖋b🖋🔒🔑a🖋y🖋🔏b🖋a🖋P*
!P	🖋a🖋🔑a🖋a🖋P**

* Here, names a and b are disposed, that is, they are bound and cannot be accessed afterwards. This does not impact the result of the program, since the amount of possible names within a program is not finite, and a and b can simply be avoided afterwards.

** Here, name a, as well as every possible decrypted version of name a, is disposed. Similarly to above, this does not impact the ability to embed π-calculus within Padlock.

These substitutions are non-trivial, because unlike in π-calculus, sending a name in Padlock sends an encrypted name instead, which can only be decrypted using 🔑, which in turn replicates the process indefinitely. This replication is avoided by abusing the synchronicity of communication in Padlock; 🔏x🖋y🖋P will only execute P once it receives a name on channel x, and thus will hang indefinitely if nothing is ever sent through the channel. Similarly, as 🔑 both decrypts and replicates, if only the replication is needed (like it is for !P), a disposable name may be provided to the instruction to be "decrypted" indefinitely.