Misplaced Pages

#857142

54-406: The π -calculus has few terms and is a small, yet expressive language (see § Syntax ). Functional programs can be encoded into the π -calculus, and the encoding emphasises the dialogue nature of computation, drawing connections with game semantics . Extensions of the π -calculus, such as the spi calculus and applied π , have been successful in reasoning about cryptographic protocols . Beside

108-439: A process variable which can be instantiated by a process term. Sangiorgi established that the ability to pass processes does not increase the expressivity of the π -calculus: passing a process P can be simulated by just passing a name that points to P instead. The π -calculus is a universal model of computation . This was first observed by Milner in his paper "Functions as Processes", in which he presents two encodings of

162-404: A bound name x may be extruded by an output action, causing the scope of x to be extended. In cases where x is a free name of Q {\displaystyle Q} , alpha-conversion may be used to allow extension to proceed. We write P → P ′ {\displaystyle P\rightarrow P'} if P {\displaystyle P} can perform

216-501: A computation step, following which it is now P ′ {\displaystyle P'} . This reduction relation → {\displaystyle \rightarrow } is defined as the least relation closed under a set of reduction rules. The main reduction rule which captures the ability of processes to communicate through channels is the following: There are three additional rules: The latter rule states that processes that are structurally congruent have

270-447: A connection to the term M {\displaystyle M} . Game semantics Game semantics ( German : dialogische Logik , translated as dialogical logic ) is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes . In

324-402: A formal footing by extending the π -calculus with arbitrary datatypes. Below is a tiny example of a process which consists of three parallel components. The channel name x is only known by the first two components. The first two components are able to communicate on the channel x , and the name y becomes bound to z . The next step in the process is therefore Note that the remaining y

378-413: A general framework for the study of logical and philosophical issues related to logical pluralism . Beginning 1994 this triggered a kind of renaissance with lasting consequences. This new philosophical impulse experienced a parallel renewal in the fields of theoretical computer science , computational linguistics , artificial intelligence , and the formal semantics of programming languages , for instance

432-687: A guarded one; this fact has been used to demonstrate that the asynchronous calculus is strictly less expressive than the synchronous one (with the choice operator). The polyadic π -calculus allows communicating more than one name in a single action: x ¯ ⟨ z 1 , . . . , z n ⟩ . P {\displaystyle {\overline {x}}\langle z_{1},...,z_{n}\rangle .P} (polyadic output) and x ( z 1 , . . . , z n ) . P {\displaystyle x(z_{1},...,z_{n}).P} (polyadic input) . This polyadic extension, which

486-441: A logic with branching quantifiers . It was thought that the principle of compositionality fails for these logics, so that a Tarskian truth definition could not provide a suitable semantics. To get around this problem, the quantifiers were given a game-theoretic meaning. Specifically, the approach is the same as in classical propositional logic, except that the players do not always have perfect information about previous moves by

540-421: A process in π –calculus are defined inductively by the table below. The set of bound names of a process are defined as the names of a process that are not in the set of free names. Central to both the reduction semantics and the labelled transition semantics is the notion of structural congruence . Two processes are structurally congruent, if they are identical up to structure. In particular, parallel composition

594-703: A server spawns a new copy of the process P [ a / y ] {\displaystyle P[a/y]} , where a is the name passed by the client to the server, during the latter's invocation. A higher order π -calculus can be defined where not only names but processes are sent through channels. The key reduction rule for the higher order case is x ¯ ⟨ R ⟩ . P | x ( Y ) . Q → P | Q [ R / Y ] {\displaystyle {\overline {x}}\langle R\rangle .P|x(Y).Q\rightarrow P|Q[R/Y]} Here, Y {\displaystyle Y} denotes

SECTION 10

#1732851656858

648-400: A set of objects called names . The abstract syntax for the π -calculus is built from the following BNF grammar (where x and y are any names from Χ): In the concrete syntax below, the prefixes bind more tightly than the parallel composition (|), and parentheses are used to disambiguate. Names are bound by the restriction and input prefix constructs. Formally, the set of free names of

702-432: A state P {\displaystyle P} to some other state P ′ {\displaystyle P'} after an action α {\displaystyle \alpha } is notated as: Where states P {\displaystyle P} and P ′ {\displaystyle P'} represent processes and α {\displaystyle \alpha }

756-691: Is ∃ f ∀ x ϕ ( x , f ( x ) ) {\displaystyle \exists f\forall x\,\phi (x,f(x))} . The Skolem function f (if it exists) actually codifies a winning strategy for the Verifier of S by returning a witness for the existential sub-formula for every choice of x the Falsifier might make. The above definition was first formulated by Jaakko Hintikka as part of his GTS interpretation. The original version of game semantics for classical (and intuitionistic) logic due to Paul Lorenzen and Kuno Lorenz

810-515: Is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel composition, summation between actions and scope restriction. CCS is useful for evaluating the qualitative correctness of properties of a system such as deadlock or livelock . According to Milner, "There

864-419: Is a game-semantical approach to logic in an extreme sense, treating games as targets to be serviced by logic rather than as technical or foundational means for studying or justifying logic. Its starting philosophical point is that logic is meant to be a universal, general-utility intellectual tool for ‘navigating the real world’ and, as such, it should be construed semantically rather than syntactically, because it

918-432: Is commutative and associative. More precisely, structural congruence is defined as the least equivalence relation preserved by the process constructs and satisfying: Alpha-conversion : Axioms for parallel composition : Axioms for restriction : Axiom for replication : Axiom relating restriction and parallel : This last axiom is known as the "scope extension" axiom. This axiom is central, since it describes how

972-402: Is either an input action a ( x ) {\displaystyle a(x)} , an output action a ¯ ⟨ x ⟩ {\displaystyle {\overline {a}}\langle x\rangle } , or a silent action τ . A standard result about the labelled semantics is that it agrees with the reduction semantics up to structural congruence, in

1026-593: Is encoded as ( ν w ) x ¯ ⟨ w ⟩ . w ¯ ⟨ y 1 ⟩ . ⋯ . w ¯ ⟨ y n ⟩ . [ P ] {\displaystyle (\nu w){\overline {x}}\langle w\rangle .{\overline {w}}\langle y_{1}\rangle .\cdots .{\overline {w}}\langle y_{n}\rangle .[P]} x ( y 1 , ⋯ , y n ) . P {\displaystyle x(y_{1},\cdots ,y_{n}).P}

1080-402: Is encoded as x ( w ) . w ( y 1 ) . ⋯ . w ( y n ) . [ P ] {\displaystyle x(w).w(y_{1}).\cdots .w(y_{n}).[P]} All other process constructs are left unchanged by the encoding. In the above, [ P ] {\displaystyle [P]} denotes the encoding of all prefixes in

1134-466: Is extended to cover the third component as well. This was captured using the scope extension axiom. Next, using the reduction substitution axiom, we get Finally, using the axioms for parallel composition and restriction, we get Alternatively, one may give the pi-calculus a labelled transition semantics (as has been done with the Calculus of Communicating Systems ). In this semantics, a transition from

SECTION 20

#1732851656858

1188-473: Is not affected because it is defined in an inner scope. The second and third parallel components can now communicate on the channel name z , and the name v becomes bound to x . The next step in the process is now Note that since the local name x has been output, the scope of x is extended to cover the third component as well. Finally, the channel x can be used for sending the name x . After that all concurrently executing processes have stopped Let Χ be

1242-402: Is nothing canonical about the choice of the basic combinators, even though they were chosen with great attention to economy. What characterises our calculus is not the exact choice of combinators, but rather the choice of interpretation and of mathematical framework". The expressions of the language are interpreted as a labelled transition system . Between these models, bisimilarity is used as

1296-482: Is semantics that serves as a bridge between real world and otherwise meaningless formal systems (syntax). Syntax is thus secondary, interesting only as much as it services the underlying semantics. From this standpoint, Japaridze has repeatedly criticized the often followed practice of adjusting semantics to some already existing target syntactic constructions, with Lorenzen ’s approach to intuitionistic logic being an example. This line of thought then proceeds to argue that

1350-517: Is to propositional logic . Each formula of this language is interpreted as a game between two players, known as the "Verifier" and the "Falsifier". The Verifier is given "ownership" of all the disjunctions in the formula, and the Falsifier is likewise given ownership of all the conjunctions . Each move of the game consists of allowing the owner of the principal connective to pick one of its branches; play will then continue in that subformula, with whichever player controls its principal connective making

1404-473: Is useful especially when studying types for name passing processes, can be encoded in the monadic calculus by passing the name of a private channel through which the multiple arguments are then passed in sequence. The encoding is defined recursively by the clauses x ¯ ⟨ y 1 , ⋯ , y n ⟩ . P {\displaystyle {\overline {x}}\langle y_{1},\cdots ,y_{n}\rangle .P}

1458-503: The dialogical approach to the study of several non-classical logics such as modal logic , relevance logic , free logic and connexive logic . Recently, Rahman and collaborators developed the dialogical approach into a general framework aimed at the discussion of logical pluralism. Foundational considerations of game semantics have been more emphasised by Jaakko Hintikka and Gabriel Sandu, especially for independence-friendly logic (IF logic, more recently information -friendly logic),

1512-449: The halting problem and exceeds the reasoning abilities of human agents. GTS avoids this with a rule to test formulas against an underlying model; logical dialogues, with a non-repetition rule (similar to threefold repetition in Chess). Genot and Jacot (2017) proved that players with severely bounded rationality can reason to terminate a play without IEDS. For most common logics, including

1566-429: The lambda-calculus in the π -calculus. One encoding simulates the eager (call-by-value) evaluation strategy , the other encoding simulates the normal-order (call-by-name) strategy. In both of these, the crucial insight is the modeling of environment bindings – for instance, " x is bound to term M {\textstyle M} " – as replicating agents that respond to requests for their bindings by sending back

1620-435: The Falsifier for universal quantifiers ) and its bound variable replaced at all occurrences by an object of the owner's choosing, drawn from the domain of quantification. Note that a single counterexample falsifies a universally quantified statement, and a single example suffices to verify an existentially quantified one. Assuming the axiom of choice , the game-theoretical semantics for classical first-order logic agree with

1674-495: The calculus, this and related extensions are often useful. The asynchronous π -calculus allows only outputs with no continuation, i.e. output atoms of the form x ¯ ⟨ y ⟩ {\displaystyle {\overline {x}}\langle y\rangle } , yielding a smaller calculus. However, any process in the original calculus can be represented by the smaller asynchronous π -calculus using an extra channel to simulate explicit acknowledgement from

π-calculus - Misplaced Pages Continue

1728-535: The context of proof theory, where the so-called reduction rules (showing the effect of elimination rules on the result of introduction rules) should be seen as appropriate to formalise the explanation of the (immediate) consequences one can draw from a proposition, thus showing the function/purpose/usefulness of its main connective in the calculus of language ( de Queiroz (1988) , de Queiroz (1991) , de Queiroz (1994) , de Queiroz (2001) , de Queiroz (2008) , de Queiroz (2023) ). The simplest application of game semantics

1782-743: The continuation P {\displaystyle P} in the same way. The full power of replication ! P {\displaystyle !P} is not needed. Often, one only considers replicated input ! x ( y ) . P {\displaystyle !x(y).P} , whose structural congruence axiom is ! x ( y ) . P ≡ x ( y ) . P | ! x ( y ) . P {\displaystyle !x(y).P\equiv x(y).P|!x(y).P} . Replicated input process such as ! x ( y ) . P {\displaystyle !x(y).P} can be understood as servers, waiting on channel x to be invoked by clients. Invocation of

1836-488: The definition of strategies inductively on the syntax. Using game semantics, the authors mentioned above have solved the long-standing problem of defining a fully abstract model for the programming language PCF . Consequently, game semantics has led to fully abstract semantic models for a variety of programming languages, and to new semantic-directed methods of software verification by software model checking . Shahid Rahman  [ fr ] and Helge Rückert extended

1890-434: The formula contains negations or implications, other, more complicated, techniques may be used. For example, a negation should be true if the thing negated is false, so it must have the effect of interchanging the roles of the two players. More generally, game semantics may be applied to predicate logic ; the new rules allow a principal quantifier to be removed by its "owner" (the Verifier for existential quantifiers and

1944-452: The late 1950s Paul Lorenzen was the first to introduce a game semantics for logic , and it was further developed by Kuno Lorenz . At almost the same time as Lorenzen, Jaakko Hintikka developed a model-theoretical approach known in the literature as GTS (game-theoretical semantics). Since then, a number of different game semantics have been studied in logic. Shahid Rahman ( Lille III ) and collaborators developed dialogical logic into

1998-826: The machine's winning strategies for them as solutions to those problems. It has been established that computability logic is robust with respect to reasonable variations in the complexity of allowed strategies, which can be brought down as low as logarithmic space and polynomial time (one does not imply the other in interactive computations) without affecting the logic. All this explains the name “computability logic” and determines applicability in various areas of computer science. Classical logic , independence-friendly logic and certain extensions of linear and intuitionistic logics turn out to be special fragments of computability logic, obtained merely by disallowing certain groups of operators or atoms. Calculus of Communicating Systems The calculus of communicating systems ( CCS )

2052-409: The next move. Play ends when a primitive proposition has been so chosen by the two players; at this point the Verifier is deemed the winner if the resulting proposition is true, and the Falsifier is deemed the winner if it is false. The original formula will be considered true precisely when the Verifier has a winning strategy , while it will be false whenever the Falsifier has the winning strategy. If

2106-462: The normal sense, it is easy to extend the calculus. In particular, it is easy to define both control structures such as recursion, loops and sequential composition and datatypes such as first-order functions, truth values , lists and integers. Moreover, extensions of the π -calculus have been proposed which take into account distribution or public-key cryptography. The applied π -calculus due to Abadi and Fournet [1] put these various extensions on

2160-457: The ones above, the games that arise from them have perfect information —that is, the two players always know the truth values of each primitive, and are aware of all preceding moves in the game. However, with the advent of game semantics, logics, such as the independence-friendly logic of Hintikka and Sandu, with a natural semantics in terms of games of imperfect information have been proposed. The primary motivation for Lorenzen and Kuno Lorenz

2214-476: The original use in describing concurrent systems, the π -calculus has also been used to reason about business processes and molecular biology . The π -calculus belongs to the family of process calculi , mathematical formalisms for describing and analyzing properties of concurrent computation. In fact, the π -calculus, like the λ-calculus , is so minimal that it does not contain primitives such as numbers, booleans, data structures, variables, functions, or even

π-calculus - Misplaced Pages Continue

2268-534: The other hand resulted in the work of many others, including S. Abramsky , J. van Benthem, A. Blass , D. Gabbay , M. Hyland , W. Hodges , R. Jagadeesan, G. Japaridze , E. Krabbe, L. Ong, H. Prakken, G. Sandu, D. Walton, and J. Woods, who placed game semantics at the center of a new concept in logic in which logic is understood as a dynamic instrument of inference. There has also been an alternative perspective on proof theory and meaning theory, advocating that Wittgenstein 's "meaning as use" paradigm as understood in

2322-482: The other player. Wilfrid Hodges has proposed a compositional semantics and proved it equivalent to game semantics for IF-logics. More recently Shahid Rahman  [ fr ] and the team of dialogical logic in Lille implemented dependences and independences within a dialogical framework by means of a dialogical approach to intuitionistic type theory called immanent reasoning . Japaridze ’s computability logic

2376-408: The receiving process. Since a continuation-free output can model a message-in-transit, this fragment shows that the original π -calculus, which is intuitively based on synchronous communication, has an expressive asynchronous communication model inside its syntax. However, the nondeterministic choice operator defined above cannot be expressed in this way, as an unguarded choice would be converted into

2430-410: The same reductions. Consider again the process Applying the definition of the reduction semantics, we get the reduction Note how, applying the reduction substitution axiom, free occurrences of y {\displaystyle y} are now labeled as z {\displaystyle z} . Next, we get the reduction Note that since the local name x has been output, the scope of x

2484-509: The semantics, in turn, should be a game semantics, because games “offer the most comprehensive, coherent, natural, adequate and convenient mathematical models for the very essence of all ‘navigational’ activities of agents: their interactions with the surrounding world”. Accordingly, the logic-building paradigm adopted by computability logic is to identify the most natural and basic operations on games, treat those operators as logical operations, and then look for sound and complete axiomatizations of

2538-499: The sense that P → P ′ {\displaystyle P\rightarrow P'} if and only if P → τ ≡ P ′ {\displaystyle P\,\xrightarrow {\overset {}{\tau }} \equiv P'} The syntax given above is a minimal one. However, the syntax may be modified in various ways. A nondeterministic choice operator P + Q {\displaystyle P+Q} can be added to

2592-485: The sets of game-semantically valid formulas. On this path a host of familiar or unfamiliar logical operators have emerged in the open-ended language of computability logic, with several sorts of negations, conjunctions, disjunctions, implications, quantifiers and modalities. Games are played between two agents: a machine and its environment, where the machine is required to follow only computable strategies. This way, games are seen as interactive computational problems, and

2646-520: The syntax. A test for name equality [ x = y ] P {\displaystyle [x=y]P} can be added to the syntax. This match operator can proceed as P {\displaystyle P} if and only if x and y {\displaystyle y} are the same name. Similarly, one may add a mismatch operator for name inequality . Practical programs which can pass names (URLs or pointers) often use such functionality: for directly modeling such functionality inside

2700-409: The usual model-based (Tarskian) semantics . For classical first-order logic the winning strategy for the Verifier essentially consists of finding adequate Skolem functions and witnesses . For example, if S denotes ∀ x ∃ y ϕ ( x , y ) {\displaystyle \forall x\exists y\,\phi (x,y)} then an equisatisfiable statement for S

2754-451: The usual control flow statements (such as if-then-else , while ). Central to the π -calculus is the notion of name . The simplicity of the calculus lies in the dual role that names play as communication channels and variables . The process constructs available in the calculus are the following (a precise definition is given in the following section): Although the minimalism of the π -calculus prevents us from writing programs in

SECTION 50

#1732851656858

2808-450: The work of Johan van Benthem and collaborators in Amsterdam who looked thoroughly at the interface between logic and games, and Hanno Nickau who addressed the full abstraction problem in programming languages by means of games. New results in linear logic by Jean-Yves Girard in the interfaces between mathematical game theory and logic on one hand and argumentation theory and logic on

2862-672: Was not defined in terms of models but of winning strategies over formal dialogues (P. Lorenzen, K. Lorenz 1978, S. Rahman and L. Keiff 2005). Shahid Rahman and Tero Tulenheimo developed an algorithm to convert GTS-winning strategies for classical logic into the dialogical winning strategies and vice versa. Formal dialogues and GTS games may be infinite and use end-of-play rules rather than letting players decide when to stop playing. Reaching this decision by standard means for strategic inferences ( iterated elimination of dominated strategies or IEDS) would, in GTS and formal dialogues, be equivalent to solving

2916-573: Was to find a game-theoretic (their term was dialogical , in German Dialogische Logik  [ de ] ) semantics for intuitionistic logic . Andreas Blass was the first to point out connections between game semantics and linear logic . This line was further developed by Samson Abramsky , Radhakrishnan Jagadeesan , Pasquale Malacaria and independently Martin Hyland and Luke Ong , who placed special emphasis on compositionality, i.e.

#857142