1 #LyX 1.3 created this file. For more info see http://www.lyx.org/

2 \lyxformat 221

3 \textclass article

4 \language english

5 \inputencoding auto

6 \fontscheme palatino

7 \graphics default

8 \paperfontsize default

9 \spacing single

10 \papersize a4paper

11 \paperpackage widemarginsa4

12 \use_geometry 0

13 \use_amsmath 0

14 \use_natbib 0

15 \use_numerical_citations 0

16 \paperorientation portrait

17 \secnumdepth 3

18 \tocdepth 3

19 \paragraph_separation indent

20 \defskip medskip

21 \quotes_language english

22 \quotes_times 2

23 \papercolumns 2

24 \papersides 1

25 \paperpagestyle default

26

27 \layout Title

28

29 Pseudo-ambients

30 \layout Author

31

32 Tony Garnock-Jones <tonyg@kcbbs.gen.nz>

33 \layout Date

34

35 1 November 2004

36 \layout Standard

37

38 The idea is to take a calculus much like Cardelli's Mobile Ambients, and

39 short-circuit the routing so that paths are one element long and always

40 take you directly to the given port.

41

42 \begin_inset Formula $\nu$

43 \end_inset

44

45 is interpreted as allocation; the store holds allocated ports.

46 Ports/locations have exactly one parent, except for the top location,

47 \begin_inset Formula $\top$

48 \end_inset

49

50 , which has no parent.

51 The parent of a location is the location at which the

52 \begin_inset Formula $\nu$

53 \end_inset

54

55 was executed.

56 This gives rise to a tree of locations.

57 Ports do not move once they are defined, and are garbage collected when

58 no longer referenced, in the usual manner.

59 \layout Standard

60

61

62 \begin_inset Formula \begin{eqnarray*}

63 \nu x.P & & \textrm{allocation}\\

64 P\vert Q & & \textrm{par}\\

65 \left\langle \tilde{x}\right\rangle & & \textrm{output message}\\

66 (\widetilde{x}).P & & \textrm{input message}\\

67 !(\widetilde{x}).P & & \textrm{replicated input}\\

68 x[P] & & \textrm{relocation}\\

69 \mathbf{lift}\, x(y).P & & \textrm{reflection}\\

70 \mathbf{eval}\, x & & \textrm{evaluation}\end{eqnarray*}

71

72 \end_inset

73

74

75 \layout Standard

76

77 Processes are written with an environment

78 \begin_inset Formula \[

79 \mathcal{E}\subset\{ x\mapsto a\,\vert\, x,a\in\mathcal{L}\}\]

80

81 \end_inset

82

83 with ports/locations

84 \begin_inset Formula $a,b,c,\top\in\mathcal{L}$

85 \end_inset

86

87 , and processes

88 \begin_inset Formula $P$

89 \end_inset

90

91 ,

92 \begin_inset Formula $Q$

93 \end_inset

94

95 ,

96 \begin_inset Formula $R$

97 \end_inset

98

99 :

100 \layout Standard

101

102

103 \begin_inset Formula \[

104 \mathcal{E}\vdash a[P]\,\Vert\, b[Q]\,\Vert\, c[R]\]

105

106 \end_inset

107

108

109 \layout Standard

110

111 so reduction proceeds as in figure

112 \begin_inset LatexCommand \ref{cap:Reduction-rules}

113

114 \end_inset

115

116 , where

117 \begin_inset Formula $\sigma$

118 \end_inset

119

120 are appropriate substitutions.

121 Note that the rule for lift is currently not very well defined.

122 \layout Standard

123

124

125 \begin_inset Float figure

126 wide true

127 collapsed false

128

129 \layout Standard

130

131

132 \begin_inset Formula \begin{align*}

133 \mathcal{E}\vdash a[\nu x.P] & \rightarrow\mathcal{E}\cup\{ x\mapsto a\}\vdash a[P] & \textrm{R-alloc}\\

134 \mathcal{E}\vdash a[P\vert Q] & \rightarrow\mathcal{E}\vdash a[P]\Vert a[Q] & \textrm{R-par}\\

135 \mathcal{E}\vdash a[\langle\tilde{x}\rangle]\,\Vert\, a[(\tilde{y}).P] & \rightarrow\mathcal{E}\vdash a[P\sigma] & \textrm{R-comm}\\

136 \mathcal{E}\vdash a[\langle\tilde{x}\rangle]\,\Vert\, a[!(\tilde{y}).P] & \rightarrow\mathcal{E}\vdash a[P\sigma]\,\Vert\, a[!(\tilde{y}).P] & \textrm{R-repcomm}\\

137 \mathcal{E}\vdash a[x[P]] & \rightarrow\mathcal{E}\vdash x[P] & \textrm{R-reloc}\\

138 \frac{\alpha=\{ a\vert a\mapsto x\in\mathcal{E}\},\,\mathbf{P}=x[P_{0}]\,\Vert\,{\displaystyle \prod_{a\in\alpha}}a[P_{a}]}{\mathcal{E}\lyxlock\vdash a[\mathbf{lift\,}x(y).P]\,\Vert\,\mathbf{P}} & \rightarrow\mathcal{E}\cup\{ y\mapsto a\}\vdash a[P\sigma]\,\Vert\,\left\lceil \mathbf{P}\right\rceil ^{y} & \textrm{R-reflect}\end{align*}

139

140 \end_inset

141

142

143 \layout Caption

144

145

146 \begin_inset LatexCommand \label{cap:Reduction-rules}

147

148 \end_inset

149

150 Reduction rules

151 \end_inset

152

153

154 \the_end