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.
# 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.
# 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 	🔒
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.
Category:Languages Category:Functional paradigm Category:Turing complete Category:Turing tarpits Category:No IO Category:Thematic