4. Kommunenes forventninger til næringslivets vurdering av ”sin” kommune i bedriftsutviklingssammenheng
4.9 Hva tror du brukerne vil krysse av som viktig for etablering / lokalisering / videreutvikling (videre satsing) i NN
Demonstra¸c˜ao. Por indu¸c˜ao na estrutura das λσ-nfs, descrita no Lema 3.3.8.
• Se N ≡ 1, nada h´a provar.
• Sejam N ≡ 1 [↑n] e τ ∈ T . Pelo Lema 8.1.2.2, 1 [↑n] : hωn.τ.nil ` τ i.
• Seja N ≡ 1 N1· · · Nm. Por HI tem-se que ∀1 ≤ i ≤ m, Ni ´e tip´avel em λσr∧ ent˜ao seja
Ni: hΓi ` σii. Seja τ = σ1→ · · · → σm→ β ent˜ao, por (var), 1 : hτ.nil ` τ i. Assim,
pela regra →e aplicada m-vezes, 1 N1· · · Nm: h(ωn.τ.nil) ∧ Γ1∧ · · · ∧ Γm ` βi.
• Seja N ≡ 1 [↑n] N
1· · · Nm. Por HI, ∀1≤i≤m, Ni ´e tip´avel em λσr∧ ent˜ao seja
Ni : hΓi ` σii e seja τ = σ1 → · · · → σm → β. Portanto, pelo Lema 8.1.2.2
tem-se que 1 [↑n] : hωn.τ.nil ` τ i e, por m aplica¸c˜oes de →
e, 1 [↑n] N1· · · Nm :
h(ωn.τ.nil) ∧ Γ1∧ · · · ∧ Γm ` βi.
• Seja N ≡ λ.N0. Por HI, N0: hΓ0 ` σi. Se Γ0 = u.Γ ent˜ao, por →
i, λ.N0: hΓ ` u → σi.
Sen˜ao, por →0i, λ.N0: hnil ` ω → σi.
• Seja S ≡ N1. · · · .Nm. ↑n, onde m 6= n. Por HI tem-se que ∀1≤i≤m, Ni ´e tip´a-
vel ent˜ao seja Ni : hΓi ` σii. Se n > 0 ent˜ao, pelo Lema 8.1.21, ↑n : hωn.Γ B
Γi para qualquer contexto Γ. Assim, pela regra (cons) m-vezes, N1. · · ·.Nm.↑n :
hΓ1∧ · · · ∧ Γm∧ (ωn.Γ) B σ
1. · · · σm.Γi. Analogamente, com a regras (id) e (cons),
N1. · · ·.Nm.id : hΓ1∧ · · · ∧ Γm∧ Γ B σ1. · · · σm.Γi.
8.2
O sistema λσ
∧e propriedades
Introduzimos nesta se¸c˜ao o sistema de IT proposto ao λσ-calculus, o λσ∧, onde algumas de suas propriedades s˜ao apresentadas. Ao contr´ario do sistema λσr∧, o sistema λσ∧ possui a propriedade de SR. Al´em disso, estabelecemos uma propriedade relacionada `a relevˆancia. Assim como para o sistema λs∧ em rela¸c˜ao ao sistema λsSM
, introduzidos no Cap´ıtulo 7, as altera¸c˜oes propostas ao sistema λσr∧ para a obten¸c˜ao de um sistema de IT com a propriedade de SR para o λσ, impedem a caracteriza¸c˜ao de SN de uma λσ-express˜ao atrav´es da tipabilidade no sistema. A seguir, apresentamos a defini¸c˜ao do sistema λσ∧.
8.2 O sistema λσ∧ e propriedades 162 Defini¸c˜ao 8.2.1 (O sistema λσ∧): As regras para tipagem no sistema λσ∧ s˜ao dadas a seguir, onde m > 0 e n ≥ 0: 1 : hτ.nil ` τ i (var) M : hu.Γ ` τ i λ.M : hΓ ` u → τ i →i M1: hΓ ` ω → τ i (M1 M2) : hΓ ` τ i →ω e M : hnil ` τ i λ.M : hnil ` ω → τ i → 0 i M1: hΓ ` ∧mi=1σi→ τ i M2: h∆1 ` σ1i . . . M2: h∆m ` σmi (M1 M2) : hΓ ∧ ∆1 ∧ · · · ∧ ∆m ` τ i →e (clos) S : hΓ B Γ 0i M : hΓ0 ` τ i M [S] : hΓ ` τ i (∧-cons) M : h∆ 1 ` σ 1i . . . M : h∆m ` σmi S : h∆ B ∆0i M.S : h∆ ∧ ∆1∧ · · · ∧ ∆m B (∧mi=1σi).∆0i (id) Γ 6= ∆.ω m id : hΓ B Γi (comp) S : hΓ B Γ00i S0: hΓ00B Γ0i S0◦ S : hΓ B Γ0i (nil-shift)
↑ : hnil B nili (nil-cons)
S : h∆ B nili M.S : h∆ B nili (ω-shift) Γ 6= ∆.ω n ↑ : hω.Γ B Γi (ω-cons) S : h∆ B ∆0i M.S : h∆ B ω.∆0i, ∆ 0 6= ωn
Note que a premissa para a regra (ω-shift) foi alterada de forma a excluir, al´em de qualquer contexto omega, qualquer contexto que termine com um contexto omega. Uma premissa similar sobre contextos foi inclu´ıda para (id). Note que (id) n˜ao exclui Γ = nil enquanto que (ω-shift) exclui essa possibilidade. Essas condi¸c˜oes extra garantem que toda substitui¸c˜ao, e n˜ao apenas as aplicadas a termos, tenham a propriedade apresentada no lema a seguir.
Lema 8.2.2: Se M : hΓ `λσ∧ τ i e m = |Γ| > 0, ent˜ao Γm6= ω. Em particular, se S : hΓ B Γ0i
e m = |Γ| > 0 ent˜ao Γm6= ω e se m0= |Γ0| > 0 ent˜ao Γ0m06= ω.
Demonstra¸c˜ao. A demonstra¸c˜ao ´e feita por indu¸c˜ao em M : hΓ ` τ i, com subindu¸c˜ao em S : hΓ B Γ0i. A prova para as regras (var), →i, →e e →ωe s˜ao similares as provas no Lema
8.2 O sistema λσ∧ e propriedades 163 • Se Γ 6= ∆.ω
m
id : hΓ B Γi, nada h´a provar. • Se ↑ : hnil B nili, nada h´a provar. • Se Γ 6= ∆.ω
n
↑ : hω.Γ B Γi, nada h´a provar. • Seja S : h∆ B nili
M.S : h∆ B nili. Se m = |∆| > 0, ent˜ao por HI tem-se que ∆m6= ω.
• Seja S : h∆ B ∆
0i
M.S : h∆ B ω.∆0i, ∆
0 6= ωn. Por HI tem-se que se m = |∆| > 0, ent˜ao ∆
m6= ω e
para m0= |∆0| tem-se que ∆0
m06= ω. Assim, |ω.∆0| = m0+1 e (ω.∆0)m0+1= ∆0 m06= ω. • Seja M : h∆ 1 ` σ 1i . . . M : h∆m ` σmi S : h∆ B ∆0i M.S : h∆ ∧ ∆1∧ · · · ∧ ∆m B (∧mi=1σi).∆0i
. Por HI tem-se que se m0= |∆0| > 0 ent˜ao ∆0
m0 6= ω. Note que |∆ ∧ ∆1∧ · · · ∧ ∆m| = max(|∆|, |∆1|, . . . , |∆m|). Assim, se m = |∆ ∧ ∆1∧ · · · ∧ ∆m| > 0, ent˜ao basta tomar algum contexto de
comprimento m e mostrar que ele satisfaz a propriedade. Suponha s.p.d.g. que |∆| = m. Portanto, por HI tem-se que se m = |∆| > 0, ent˜ao ∆m6= ω.
• Seja S : hΓ B Γ
00i
S0: hΓ00B Γ0i
S0◦ S : hΓ B Γ0i . Por HI tem-se que se m = |Γ| > 0 ent˜ao Γm6= ω e se m0= |Γ0| > 0 ent˜ao Γ0m06= ω.
• Seja S : hΓ B Γ
0i
M : hΓ0 ` τ i
M [S] : hΓ ` τ i . Por HI tem-se que se m = |Γ| > 0 ent˜ao Γm6= ω. Note que a prova para substitui¸c˜oes tem como base as tipagens de id e ↑. Portanto, as condi¸c˜oes para contextos adicionadas nas premissas ´e essencial.
Corol´ario 8.2.3: Se M : hΓ `λσ∧ τ i, ent˜ao Γ 6= ∆.ωm, para quaisquer contexto ∆ e m > 0. Em particular, se S : hΓ Bλσ∧Γ0i ent˜ao Γ 6= ∆.ωm e Γ06= ∆0.ωm, para quaisquer contextos ∆ e ∆0 e m > 0.
As novas condi¸c˜oes para contexto garantem a propriedade apresentada no Corol´ario 8.2.3 acima, para toda substitui¸c˜ao tip´avel em λσ∧. Essa propriedade n˜ao ´e necess´aria para garantir a propriedade de SR. Para tal, basta adicionar a premissa Γ 6= ωm para (id), onde m > 0. Nesse caso o Lema 8.2.2, e consequentemente o corol´ario acima, ´e v´alido para termos e apenas para substitui¸c˜oes aplicadas a termos. A seguir apresentamos os lemas de gera¸c˜ao para o sistema, separados em gera¸c˜ao para substitui¸c˜oes e para termos.
8.2 O sistema λσ∧ e propriedades 164 Lema 8.2.4 (Gera¸c˜ao para substitui¸c˜oes em λσ∧):
1. S : hnil B nili para qualquer substitui¸c˜ao S. 2. Se M.S : hΓ B nili ent˜ao S : hΓ B nili.
3. Se M.S : hΓ B ω.Γ0i ent˜ao S : hΓ B Γ0i e Γ0 6= ωn.
4. Se M.S : hΓ B Γ0i e Γ0
= ∧mi=1σi.Γ00 ent˜ao S : hΓ000 B Γ00i e ∀1 ≤ i ≤ m, M : hΓi ` σii tal
que Γ = Γ000∧ Γ1∧ · · · ∧ Γm.
5. Se S : hΓ B nili ent˜ao Γ = nil.
6. ↑m: hΓ B Γ0i se, e somente se, Γ = Γ0 = nil ou Γ = ωm.Γ0, onde Γ0 6= ∆.ωn.
7. Se S : hΓ B Γ0i e S : h∆ B ∆0i ent˜
ao S : hΓ ∧ ∆ B Γ0∧ ∆0i.
8. Se S : hΓ B ∆1∧ ∆2i para ∆16= ∆0.ωm e ∆26= ∆00.ωm, ent˜ao Γ = Γ1 ∧ Γ2 tal que
S : hΓ1B ∆1i e S : hΓ2B ∆2i.
Demonstra¸c˜ao. 1. Por indu¸c˜ao na estrutura de S.
2. Suponha que M.S : hΓ B nili. Por an´alise de casos, a ´unica possibilidade para o ´
ultimo passo da deriva¸c˜ao ´e a regra (nil-cons). Portanto, S : hΓ B nili.
3. Suponha que M.S : hΓBω.Γ0i. Por an´alise de casos, o ´ultimo passo ´e a regra (ω-cons). Portanto, S : hΓ B Γ0i e Γ 6= ωn.
4. Por an´alise de casos a ´unica regra poss´ıvel no ´ultimo passo da dedu¸c˜ao ser´a a regra (∧-cons), validando a afirma¸c˜ao.
5. Por indu¸c˜ao na estrutura de S. Suponha que S : hΓ B nili. • Se S ≡ id ou S ≡ ↑, nada h´a provar.
• Se S ≡ S1◦ S2, ent˜ao por (comp) tem-se que S1: hΓ0 ` nili e S2: hΓ ` Γ0i. Por
HI em S1 tem-se que Γ0= nil e, por HI em S2, tem-se Γ = nil.
• Se S ≡ M.S0 ent˜ao, pelo item 2, S0
8.2 O sistema λσ∧ e propriedades 165 6. Se Γ0= nil ent˜ao pelo item 5 acima tem-se que Γ = nil. Sen˜ao a hip´otese ´e provada
por indu¸c˜ao em m.
7. Por indu¸c˜ao na estrutura de S. Suponha que S : hΓ B Γ0i e que S : h∆ B ∆0i. Observe que se Γ0= nil ou ∆0= nil ent˜ao, pelo item 5, Γ = nil e ∆ = nil, respectivamente, e a afirma¸c˜ao ´e verdadeira. Assim, consideram-se apenas os casos onde Γ0, ∆06= nil.
• Se S ≡ id, ent˜ao por (id) tem-se que Γ = Γ0 e ∆ = ∆0 e Γ 6= Γ00.ωm e ∆ 6= ∆00.ωm, para qualquer m > 0. Assim, Γ∧∆ 6= Γ00.ωm logo, por (id), id : hΓ ∧ ∆ ` Γ0∧ ∆0i
onde Γ0∧ ∆0= Γ ∧ ∆.
• Seja S ≡↑ e suponha que Γ0, ∆0 6= nil. Ent˜ao pelo item 6 tem-se que Γ = ω.Γ0 e
∆ = ω.∆0, onde Γ06= Γ00.ωne ∆06= ∆00.ωn. Tem-se que (ω.Γ0)∧(ω.∆0) = ω.(Γ0∧∆0)
logo, por (ω-shift), ↑ : hΓ ∧ ∆ B Γ0∧ ∆0i.
• Seja S ≡ S1 ◦ S2. Por (comp) tem-se que S1 : hΓ00 B Γ0i, S2: hΓ B Γ00i, S1 :
h∆00
B ∆0i e S2 : h∆ B ∆00i. Por HI tem-se que S1 : hΓ00∧ ∆00 B Γ0∧ ∆0i e
S2: hΓ ∧ ∆ B Γ00∧ ∆00i logo, por (comp), S1◦ S2: hΓ ∧ ∆ B Γ0∧ ∆0i.
• Seja S ≡ M.S0. Suponha s.p.d.g. que Γ0 = ω.Γ00 e ∆0 = (∧m
i=1σi).∆00.
Pelo item 3 tem-se que S0 : hΓ B Γ00i para Γ00 6= ωn. Pelo item 4 tem-se
que S0 : h∆000 B ∆00i onde ∆ = ∆000 ∧ ∆1∧ · · · ∧ ∆m e ∀1 ≤ i ≤ m, M :
h∆i ` σ
ii. Assim, por HI, S0 : hΓ ∧ ∆000 B Γ00∧ ∆00i e por (∧-cons) tem-
se que M.S0 : h(Γ ∧ ∆000) ∧ ∆1 ∧ · · · ∧ ∆m B ∧m
i=1σi.(Γ00∧ ∆00)i. Observe que
(Γ ∧ ∆000) ∧ ∆1∧ · · · ∧ ∆m = Γ ∧ (∆000∧ ∆1∧ · · · ∧ ∆m) = Γ ∧ ∆.
8. Por indu¸c˜ao na estrutura de S. Suponha que S : hΓB∆1∧ ∆2i. Note que se ∆j = nil
para j ∈ {1, 2} ent˜ao, pelo item 1, S : hΓj B ∆ji para Γj= nil e a afirma¸c˜ao ´e trivial.
Consideram-se os casos onde ∆1, ∆26= nil.
• Se S ≡ id, ent˜ao por (id) tem-se que Γ = ∆1 ∧ ∆2. Assim, seja Γj= ∆j para
j ∈ {1, 2}. Logo por (id) tem-se que id : h∆j B ∆ji.
• Seja S ≡↑. Pelo item 6 tem-se que Γ = ω.(∆1∧ ∆2). Assim, para Γ1= ω.∆1 e
Γ2= ω.∆2 tem-se o resultado.
• Seja S ≡ S1 ◦ S2. Por (comp) tem-se que S1: hΓ0 B ∆1∧ ∆2i e S2: hΓ B Γ0i.
Por HI tem-se que Γ0= (Γ0)1∧ (Γ0)2 tal que S
8.2 O sistema λσ∧ e propriedades 166 Pelo Corol´ario 1 tem-se que (Γ0)16= (Γ00)1.ωm e (Γ0)26= (Γ00)2.ωm, para qualquer
m > 0. Assim, por HI tem-se que Γ = Γ1 ∧ Γ2 tal que S
2 : hΓ1 B (Γ0)1i e
S2: hΓ2B (Γ0)2i. Portanto, por (comp), S1◦ S2: hΓ1B ∆1i e S1◦ S2: hΓ2B ∆2i.
• Seja S ≡ M.S0. Suponha s.p.d.g. que ∆1= ω.∆0 e que ∆2= (∧m
i=1σi).∆00. Pelo
item 4 tem-se que S0: hΓ0B ∆0∧ ∆00i onde Γ = Γ0∧ Γ1∧ · · · ∧ Γm e ∀1 ≤ i ≤ m,
M : hΓi ` σ
ii. Assim, por HI, Γ0 = (Γ0)1 ∧ (Γ0)2 onde S0 : h(Γ0)1 B ∆0i e
S0: h(Γ0)2 B ∆00i. Por (ω-cons) tem-se M.S0 : h(Γ0)1 B ω.∆0i e, por (∧-cons),
M.S0: h(Γ0)2∧ Γ1∧ · · · ∧ Γm B (∧m
i=1σi).∆00i. Portanto, tomando Γ1= (Γ0)1 e
Γ2= (Γ0)2∧ Γ1∧ · · · ∧ Γm tem-se o resultado.
Lema 8.2.5 (Gera¸c˜ao para termos em λσ∧): 1. 1 [↑m] : hΓ `
λσ∧ τ i se, e somente se, Γ = ωm.τ.nil.
2. Se λ.M : hnil `λσ∧ τ i, ent˜ao τ = ω → σ e M : hnil `λσ∧ σi ou τ = ∧ni=1σi→ σ, n > 0, e
M : h∧ni=1σi.nil `λσ∧ σi onde σ, σ1, . . . , σn∈ T .
3. Se λ.M : hΓ `λσ∧ τ i e |Γ| > 0, ent˜ao τ = u → σ para algum u ∈ U e σ ∈ T , onde M : hu.Γ `λσ∧ σi.
4. Se (M1 M2) : hΓ `λσ∧ τ i ent˜ao M1: hΓ `λσ∧ ω → τ i ou M1: hΓ0 `λσ∧ ∧mi=1σi→ τ i e
∀1 ≤ i ≤ m, Ni: hΓi `λσ∧ σii onde Γ = Γ0∧ Γ1∧ · · · ∧ Γm.
Demonstra¸c˜ao. 1. Suponha que 1 [↑m] : hΓ ` τ i. Por (comp) tem-se que ↑ : hΓ B Γ0i
e 1 : hΓ0 ` τ i. Assim, por (var) tem-se que Γ0 = τ.nil logo, pelo Lema 8.2.4.6, Γ = ωm.τ.nil.
2. Por an´alise de casos na deriva¸c˜ao de λ.M : hnil ` τ i.
3. Por an´alise de casos na deriva¸c˜ao de λ.M : hΓ ` τ i, para |Γ| > 0. 4. Por an´alise de casos na deriva¸c˜ao de (M1 M2) : hΓ ` τ i.
8.2.1
Redu¸c˜ao de sujeito
Com os lemas de gera¸c˜ao apresentados acima, podemos ent˜ao estabelecer o propriedade de SR para λσ∧.
8.2 O sistema λσ∧ e propriedades 167 Teorema 8.2.6 (SR para λσ∧): Seja M um termo em λσ. Se M : hΓ `λσ∧ τ i e M −→λσ
M0 ent˜ao M0: hΓ `λσ∧ τ i. Em particular, para uma substitui¸c˜ao S em λσ, se S : hΓ Bλσ∧Γ
0i
e S −→λσ S0 ent˜ao S0: hΓ Bλσ∧Γ
0i.
Demonstra¸c˜ao. A prova ´e feita atrav´es da an´alise da propriedade em cada regra de rees- crita do c´alculo.
• Beta: Suponha que (λ.M N ) : hΓ ` τ i. Pelo Lema 8.2.5.4 tem-se duas possibilidades. Suponha que λ.M : hΓ ` ω → τ i. Se Γ = nil, ent˜ao pelo Lema 8.2.5.2 tem-se que M : hnil ` τ i. Por (id) e (nil-cons), N.id : hnil B nili. Assim, por (clos), M [N.id] : hnil ` τ i. Se |Γ| > 0 ent˜ao, pelo Lema 8.2.5.3, M : hω.Γ ` τ i. Por (id) e (ω-cons), N.id : hΓ B ω.Γi logo, por (clos), M [N.id] : hΓ ` τ i.
Suponha que λ.M : hΓ0 ` ∧m
i=1σi→ τ i e ∀1 ≤ i ≤ m, N : hΓi ` σii onde Γ = Γ0 ∧
Γ1∧ · · · ∧ Γm. Pelos Lemas 8.2.5.2 e 8.2.5.3, M : h(∧m
i=1σi).Γ0 ` τ i. Assim, por (id)
e (∧-cons), N.id : hΓ0 ∧ Γ1 ∧ · · · ∧ Γm
B (∧mi=1σi).Γ0i. Portanto, por (clos), M [N.id] :
hΓ ` τ i.
• App: Suponha que (M1 M2)[S] : hΓ ` τ i. Por (clos), S : hΓ B ∆i e (M1 M2) : h∆ ` τ i.
Pelo Lema 8.2.5.4 tem-se duas possibilidades para a tipagem da aplica¸c˜ao, como descrito no caso acima.
Suponha que M1: h∆ ` ω → τ i. Por (clos) tem-se que M1[S] : hΓ ` ω → τ i. Portanto,
por →ω
e, (M1[S] M2[S]) : hΓ ` τ i.
Suponha que M1 : h∆0 ` ∧mi=1σi→ τ i e ∀1 ≤ i ≤ m, M2 : h∆i ` σii onde ∆ =
∆0∧ ∆1∧ · · · ∧ ∆m. Pelo Corol´ario 8.2.3 tem-se que ∆0, ∆1, . . . , ∆m6= ∆000.ωn, para
quaisquer contexto ∆000 e n > 0. Assim, por indu¸c˜ao em m e o Lema 8.2.4.8 tem-se que Γ = Γ0∧ Γ1∧ · · · ∧ Γm tal que S : hΓ0
B ∆0i e ∀1 ≤ i ≤ m, S : hΓi B ∆ii. Assim,
por (clos), M1[S] : hΓ0 ` (∧mi=1σi) → τ i e ∀1 ≤ i ≤ m, M2[S] : hΓi ` σii. Portanto, por
→e, (M1[S] M2[S]) : hΓ ` τ i.
• Abs: Suponha que (λ.M )[S] : hΓ ` τ i. Por (clos), S : hΓ B Γ0i e λ.M : hΓ0 ` τ i.
Se Γ0= nil ent˜ao, pelo Lema 8.2.5.2, τ = ω → τ0 e M : hnil ` τ0i ou τ = ∧m
i=1σi→ τ0
e M : h∧m
i=1σi.nil ` τ0i. Al´em disso, pelo Lema 8.2.4.5, Γ = nil. Assim, por (nil-
8.2 O sistema λσ∧ e propriedades 168 que 1 .(S ◦ ↑) : hnil B nili. Logo, por (clos), M [ 1 .(S ◦ ↑)] : hnil ` τ0i e por →0 i
tem-se que λ.M [ 1 .(S ◦ ↑)] : hnil ` τ i. Para τ = (∧mi=1σi) → τ0 tem-se por (var) e
(∧-cons) que 1 .(S ◦ ↑) : h∧m
i=1σi.nil B ∧mi=1σi.nili. Assim, por (clos) e →i tem-se que
λ.M [ 1 .(S ◦ ↑)] : hnil ` τ i.
Se |Γ0| > 0 ent˜ao pelo Corol´ario 8.2.3 tem-se que Γ0 n˜ao ´e um contexto omega e pelo Lema 8.2.5.3 tem-se que τ = u → τ0 tal que M : hu.Γ0 ` τ0i. Se Γ = nil ent˜ao por
(nil-shift) e (comp), S ◦ ↑ : hnil B Γ0i. Se u = ω ent˜ao por (ω-cons) tem-se 1 .(S ◦ ↑) : hnil B ω.Γ0i logo, por (clos) e →0
i, λ.M [ 1 .(S ◦ ↑)] : hnil ` ω → τ
0i. Se u = ∧m i=1σi
ent˜ao por (∧-cons) tem-se 1 .(S ◦ ↑) : h∧mi=1σi.nil B ∧mi=1σi.Γ0i logo, por (clos) e →i,
λ.M [ 1 .(S ◦ ↑)] : hnil ` ∧m
i=1σi→ τ0i. Se |Γ| > 0 ent˜ao, pelo Corol´ario 8.2.3, Γ 6= ∆.ωm
logo, por (ω-shift) e (comp), S ◦ ↑ : hω.Γ B Γ0i. An´alogo ao caso anterior tem-se por (ω-cons) ou (∧-cons), dependendo de u, que 1 .(S ◦ ↑) : hu.Γ B u.Γ0i. Assim, por (clos) e →i, λ.M [ 1 .(S ◦ ↑)] : hΓ ` u → τ0i.
• Clos: Suponha que (M [S])[S0] : hΓ ` τ i. Por (clos), S0
: hΓ B Γ0i e M [S] : hΓ0 ` τ i e,
por (clos) novamente, S : hΓ0B Γ00i e M : hΓ00` τ i. Portanto, por (comp) tem-se que
S ◦ S0: hΓ B Γ00i logo por (clos) tem-se que M [S ◦ S0] : hΓ ` τ i.
• V arCons: Suponha que 1 [M.S] : hΓ ` τ i. Por (clos), M.S : hΓ B Γ0i e 1 : hΓ0 ` τ i.
Por (var) tem-se que Γ0= τ.nil. Assim, pelo Lema 8.2.4.4 tem-se que S : hΓ1 B nili
onde Γ = Γ1∧ Γ2 e M : hΓ2 ` τ i. Pelo Lema 8.2.4.5 tem-se que Γ1= nil logo Γ2 = Γ.
• Id: Suponha que M [id] : hΓ ` τ i. Por (clos), id : hΓ B Γ0i e M : hΓ0 ` τ i. Por (id)
tem-se que Γ0= Γ.
• AssEnv: Suponha que (S1◦ S2) ◦ S3: hΓ B Γ0i. Por (comp) tem-se que S3: hΓ B Γ00i
e S1◦ S2 : hΓ00 B Γ0i e, por (comp) novamente, S2 : hΓ00 ` Γ000i e S1 : hΓ000 B Γ0i.
Portanto, por (comp) tem-se que S2◦ S3: hΓ ` Γ000i logo, por (comp), tem-se que
S1◦ (S2◦ S3) : hΓ B Γ0i
• M apEnv: Suponha que (M.S) ◦ S0
: hΓ B Γ0i. Por (comp) tem-se que S0
: hΓ B Γ00i e M.S : hΓ00B Γ0i.
Se Γ0= nil ent˜ao pelo Lema 8.2.4.2 tem-se que S : hΓ00 B nili. Assim, por (comp) tem-se S ◦ S0: hΓ B nili e por (nil-cons) tem-se que M[S0].(S ◦ S0) : hΓ B nili.
8.2 O sistema λσ∧ e propriedades 169 Se Γ0= ω.∆ ent˜ao pelo Lema 8.2.4.3 tem-se que S : hΓ00B∆i onde ∆ 6= ωn. Assim, por
(comp) tem-se S ◦ S0: hΓ B ∆i e por (ω-cons) tem-se que M[S0].(S ◦ S0) : hΓ B ω.∆i. Se Γ0 = ∧m
i=1σi.∆ ent˜ao pelo Lema 8.2.4.4 tem-se que S : h∆000 B ∆i onde Γ00 =
∆000 ∧ ∆1∧ · · · ∧ ∆m e ∀1 ≤ i ≤ m, M : h∆i ` σ
ii. Pelo Corol´ario 8.2.3 tem-se que
∆000, ∆1, . . . , ∆m6= Γ000.ωn, para quaisquer contexto Γ000 e n > 0. Assim, por indu¸c˜ao
em m e o Lemma 8.2.4.8 tem-se que Γ = Γ000 ∧ Γ1 ∧ · · · ∧ Γm tal que S0: hΓ000
B ∆000i e ∀1 ≤ i ≤ m, S0 : hΓi B ∆ii. Assim, por (comp) tem-se S ◦ S0 : hΓ000
B ∆i e por (clos) tem-se que ∀1 ≤i ≤ m, M [S0] : hΓi ` σii. Portanto, por (∧-cons) tem-se que
M [S0].(S ◦ S0) : hΓ000∧ Γ1∧ · · · ∧ ΓmB ∧m
i=1σi.∆i
• IdL: Suponha que id ◦ S : hΓBΓ0
i. Por (comp) tem-se que S : hΓBΓ00i e id : hΓ00
BΓ0i. Assim, por (id) tem-se que Γ00= Γ0.
• IdR: Suponha que S ◦ id : hΓBΓ0
i. Por (comp) tem-se que id : hΓBΓ00i e S : hΓ00
BΓ0i. Assim, por (id) tem-se que Γ00= Γ.
• Shif tCons: Suponha que ↑◦ (M.S) : hΓBΓ0
i. Por (comp) tem-se que M.S : hΓBΓ00i e
↑ : hΓ00
BΓ0i. Pelo Lema 8.2.4.6 tem-se que Γ0= Γ00= nil ou Γ00= ω.Γ0 onde Γ06= ∆.ωm.
Se Γ0= Γ00= nil ent˜ao pelo Lema 8.2.4.2 tem-se que S : hΓ B nili. Se Γ00= ω.Γ0 ent˜ao pelo Lema 8.2.4.3 tem-se que S : hΓ B Γ0i.
• V arShif t: Suponha que 1 .↑ : hΓ B Γ0i. Se Γ0= nil ent˜ao pelo Lema 8.2.4.5 tem-se
que Γ = nil logo, por (id), id : hnil B nili.
Se Γ0= ω.Γ00 ent˜ao pelo Lema 8.2.4.3 tem-se que ↑ : hΓ B Γ00i onde Γ006= ωn. Assim,
pelo Lema 8.2.4.6 tem-se que Γ = ω.Γ00 onde Γ006= ∆.ωn logo, por (id), id : hΓ B Γ0i
onde Γ0= ω.Γ00= Γ. Se Γ0 = ∧m
i=1σi.Γ00 ent˜ao pelo Lema 8.2.4.4 tem-se que ↑ : hΓ000 ` Γ00i onde Γ =
Γ000 ∧ Γ1∧ · · · ∧ Γm e ∀1 ≤ i ≤ m, 1 : hΓi ` σ
ii. Por (var) tem-se que ∀1 ≤ i ≤ m,
Γi= σ
i.nil. Pelo Lema 8.2.4.6 tem-se que Γ000= Γ00= nil ou Γ000= ω.Γ00para Γ006= ∆.ωn.
Em ambos os casos tem-se que Γ000∧ Γ1∧ · · · ∧ Γm = Γ000∧ (∧m
i=1σi.nil) = ∧mi=1σi.Γ00.
Portanto, id : hΓ B Γ0i.
• Scons: Suponha que 1 [S].(↑◦ S) : hΓ B Γ0i. Se Γ0 = nil ent˜ao pelo Lema 8.2.4.5
8.2 O sistema λσ∧ e propriedades 170 Se Γ0= ω.Γ00 ent˜ao pelo Lema 8.2.4.3 tem-se que ↑◦ S : hΓ B Γ00i onde Γ006= ωn. Por
(comp) tem-se que S : hΓ B ∆i e ↑ : h∆ B Γ00i. Assim, pelo Lema 8.2.4.6 tem-se ∆ = ω.Γ00 portanto S : hΓ B Γ0i.
Se Γ0 = ∧m
i=1σi.Γ00 ent˜ao pelo Lema 8.2.4.4 tem-se que ↑◦ S : hΓ000 ` Γ00i onde Γ =
Γ000 ∧ Γ1 ∧ · · · ∧ Γm e ∀1 ≤ i ≤ m, 1[S] : hΓi ` σ
ii. Por (cons) e (var) tem-se que
∀1 ≤ i ≤ m, S : hΓiB σ
i.nili. Por (comp) tem-se que S : hΓ000B ∆i e ↑ : h∆ B Γ00i. Pelo
Lema 8.2.4.6 tem-se que ∆ = Γ00= nil ou ∆ = ω.Γ00 onde Γ006= ∆0.ωn. Portanto, em
ambos os caso tem-se pelo Lema 8.2.4.7 que S : hΓ000 ∧ Γ1 ∧ · · · ∧ ΓmB∧m
Cap´ıtulo 9
Conclus˜ao e trabalhos futuros
Apresentamos neste trabalho o primeiro sistema de tipos com interse¸c˜ao (IT) para dois c´alculos de substitui¸c˜oes expl´ıctas (ES), o λσ no Cap´ıtulo 8 e o λse no Cap´ıtulo 7, e
provamos a propriedade b´asica de redu¸c˜ao de sujeito (SR) para ambos. Os sistemas de IT tˆem sido estudados como uma alternativa a sistemas de tipos baseados em Hin- dley/Milner [75], utilizado por exemplo pela implementa¸c˜ao do Standard ML [45], para o tratamento do polimorfismo em sistemas de tipos computacionais. O tratamento finit´ario para o polimorfismo em IT, listando os tipos assumidos por um mesmo procedimento, ´e conveniente computacionalmente com propriedades como a tipagem principal (PT), que permite atributos como a compila¸c˜ao separada e a recompila¸c˜ao inteligente. A proprie- dade de relevˆancia em IT ´e a forma de manter o sistema com o m´ınimo de suposi¸c˜oes poss´ıveis para a inferˆencia do par formado por um tipo e um contexto de tipo, chamado de tipagem. Al´em disso, sistemas de IT s˜ao ferramentas importantes na investiga¸c˜ao da semˆantica do λ-calculus, um estudo que ainda precisa ser realizado tanto para o λσ quanto para o λse. Os dois c´alculos de ES estudados usam uma nota¸c˜ao `a la de Bruijn, portanto
estudamos o λdB-calculus com dois sistemas de tipos com interse¸c˜ao, apresentados no
Cap´ıtulo 5. Resultados
Este trabalho apresentou um sistema de IT para os c´alculos de ES estudados, com a proposta de ser uma base para extens˜oes que incluam, e.g, a interse¸c˜ao como um construtor geral para tipos, o ω como um tipo universal, uma ordem para tipos e as vari´aveis de expans˜ao [57]. Estas ´ultimas est˜ao relacionadas com um estudo de PT em sistemas de IT
172
para c´alculos de ES. Dessa forma, no Cap´ıtulo 4 apresentamos a no¸c˜ao de PT introduzida em [98] para os c´alculos λdB, λse e λσ com sistemas de tipos simples, provados corretos e
completos de acordo `a no¸c˜ao de PT apresentada por J. Wells em [103]. O sistema λSM
dB, introduzido em [101] e apresentado na Se¸c˜ao 5.1, ´e uma vers˜ao `a la de
Bruijn do sistema λSM
de E. Sayag e M. Mauny em [37], com um regra de designa¸c˜ao de tipos para ´ındices mais geral. Analisamos a propriedade de SR para o c´alculo e provamos a propriedade para a contra¸c˜ao β atrav´es de um conceito aplic´avel em sistemas de tipos relevantes, a restri¸c˜ao para contextos.
No Cap´ıtulo 6, apresentamos uma caracteriza¸c˜ao sint´atica de PT introduzida em [101] para formas β-normais de λdB no sistema λSM rdB , uma restri¸c˜ao do sistema λ
SM
dB, seguindo a
linha do trabalho de Sayag e Mauny. Al´em da caracteriza¸c˜ao sint´atica de pares principais, similar `a de [37], conseguimos uma correspondˆencia bijetiva, m´odulo renomeamento, com PT para formas β-normais e formalizamos a correspondˆencia do contexto de uma PT e o multiconjunto de ´ındices livres de uma forma β-normal.
O sistema λudB, introduzido em [100], ´e apresentado na Se¸c˜ao 5.2, sendo este uma vers˜ao `a la de Bruijn do sistema λu de F. Kamareddine e K. Nour em [56]. Apresentamos a prova de SR para a redu¸c˜ao β neste sistema, usando uma no¸c˜ao de restri¸c˜ao de contexto mais fraca que a utilizada para o λSM
dB. Os sistemas λ
SM
dB e λ
SM r
dB s˜ao relevantes como os
sistemas originais, enquanto o sistema λudB perde a propriedade de relevˆancia presente no sistema λu, permitindo uma forma limitada de redundˆancia. Isso se deve `a combina¸c˜ao da presen¸ca de ω nos contextos, de forma a prover a estrutura sequencial necess´aria em sistemas de tipos para o λdB, e a rela¸c˜ao bin´aria para os tipos. A rela¸c˜ao de ordem para os
tipos induzida por esta rela¸c˜ao bin´aria ´e utilizada no sistema original em [56] para provar a completitude em rela¸c˜ao a semˆantica proposta. Assim, baseamos os sistemas propostos para os c´alculos de ES estudados no sistema λSM
dB, de forma a tentar obter um sistema de
IT restrito tal que as propriedades de SR e relevˆancia fossem satisfeitas. No Cap´ıtulo 7 introduzimos os sistemas λsSM e λs
e∧ de IT para o λs e λse, respecti-
vamente. A an´alise feita para a adi¸c˜ao de IT para o λse-calculus apresenta o estudo do
sistema para λs como uma etapa preliminar onde, al´em da propriedade de SR, a relevˆancia do sistema de tipos ´e considerada. A propriedade de relevˆancia ´e satisfeita para o sistema
173
λsSM com rela¸c˜ao a uma propriedade sint´atica bem definida, os ´ındices dispon´ıveis. Por outro lado, uma propriedade relacionada `a relevˆancia ´e satisfeita por λse∧, sem uma defi-
ni¸c˜ao geral para uma rela¸c˜ao com caracter´ısticas sint´aticas. A propriedade de SR para o sistema λsSM
´
e provada para o s-calculus e, com restri¸c˜ao de contexto, para a simula¸c˜ao de contra¸c˜ao β. A propriedade de SR ´e provada para λse∧ em rela¸c˜ao `a redu¸c˜ao β.
No Cap´ıtulo 8 apresentamos o estudo referente a adi¸c˜ao de IT para o λσ, introduzindo o sistema λ∧. O sistema, a exemplo do sistema de IT para o λse, tem uma propriedade
relativa `a relevˆancia sem uma rela¸c˜ao geral com caracter´ısticas sint´aticas das express˜oes em λσ. O sistema tem a propriedade de SR para a redu¸c˜ao β.
Trabalhos futuros
Apesar da defini¸c˜ao para PT de formas β-normais apresentada no Cap´ıtulo 6 ser similar a defini¸c˜ao de PT para o sistema de tipos simples λ→dB, a correspondˆencia com a no¸c˜ao geral de PT n˜ao ´e direta. Assim, fica como trabalho futuro demonstrar a correspondˆencia entre a no¸c˜ao de PT no sistema λSM r
dB e a no¸c˜ao geral de PT de Wells.
Para os sistemas de IT para o λdB baseados no sistema λSM, podemos trocar →0e do
sistema λSM dB por → ω e abaixo M : hΓ ` ω → τ i (M N ) : hΓ ` τ i → ω e
Seja λ∧dB o sistema obtido com essa troca de regras. Este sistema ´e uma vers˜ao `a la de Bruijn do sistema em [38, 39]. Com lemas de gera¸c˜ao apropriados, a exemplo dos sistemas para c´alculos de ES propostos neste trabalho e que possuem uma regra →ωe, acreditamos na possibilidade de recupera¸c˜ao das propriedades de redu¸c˜ao, e expans˜ao, de sujeito. A partir deste resultado, poderemos estender o resultado de PT para termos terminantes (WN), na linha do trabalho realizado originalmente em [38]. Assim, o λ∧dB e uma restri¸c˜ao no conjunto de tipos, a exemplo de U+ em [56], podem ser utilizados em uma caracteriza¸c˜ao de WN para o λdB. Um sistema desta forma seria um primeiro passo
para um sistema com vari´aveis de expans˜ao, formalizando tanto a substitui¸c˜ao quanto a expans˜ao para o sistema de tipos correspondente.
Para o λse-calculus, fica como trabalho futuro uma poss´ıvel prova de caracteriza¸c˜ao
para WN atrav´es da inferˆencia de tipos em λse∧ e a investiga¸c˜ao de PT para o c´alculo.
174
Podemos ainda investigar sistemas de IT para o λυ de P. Lescanne [70], permitindo uma compara¸c˜ao com o sistema λσ∧ an´aloga `a compara¸c˜ao entre propriedades para os sistemas de λs e λse, presentes neste documento. Uma quest˜ao interessante ´e se um sistema de
IT para a variante do λσ sem a regra (V arShif t) tem alguma propriedade diferente do que para a vers˜ao analisada no presente trabalho. Al´em disso, ficam as quest˜oes de caracteriza¸c˜ao de WN para o λσ atrav´es de λσ∧ e PT em sistemas com IT para λσ.
Por fim, o uso de sistemas de IT para o estudo da semˆantica dos c´alculos `a la de Bruijn, investigados no presente trabalho, devem utilizar como base os sistemas aqui introduzidos. Estes sistemas devem ser estendidos de forma a incluir uma regra de inferˆencia para a introdu¸c˜ao da interse¸c˜ao sendo esta tratada como um construtor de tipos mais geral, o ω ser tratado como um tipo universal e a inclus˜ao de uma ordem para tipos com uma regra de inferˆencia associada. Portanto, os sistemas assim obtidos devem estar relacionados ao sistema λudB, da Se¸c˜ao 5.2.
Referˆencias Bibliogr´aficas
[1] Mart´ın Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques L´evy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.
[2] Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Intersection types and lambda models. Theoretical Computer Science, 355(2):108–126, 2006. [3] Mauricio Ayala-Rinc´on and Fairouz Kamareddine. Unification via λse-style of ex-
plicit substitution. The Logical Journal of the Interest Group in Pure and Applied Logics, 9(4):489–523, 2001.
[4] Mauricio Ayala-Rinc´on and C´esar Mu˜noz. Explicit substitutions and all that. Co- lombian Journal of Computation, 1(1):47–71, 2000.
[5] Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge Univer- sity Press, New York, NY, USA, 1998.
[6] Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics (revised edi- tion), volume 103 of Studies in Logic and the Foundations of Mathematics. Elsevier Science, Amsterdan, The Netherlands, 1984.
[7] Henk Barendregt. Lambda calculi with types. In Handbook of logic in compu- ter science (vol. 2): background: computational structures, pages 117–309. Oxford University Press, New York, NY, USA, 1992.
[8] Henk Barendregt. The impact of the lambda calculus. Bulletin of Symbolic Logic, 3(2):181–215, 1997.
[9] Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Bulletin of Symbolic Logic, 48:931–940, 1983.
176
[10] Yves Bertot and Pierre Cast´eran. Interactive Theorem Proving and Program Deve- lopment. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004.
[11] Roel Bloo and Kristoffer H. Rose. Preservation of strong normalization in named lambda calculi with explicit substitution and garbage collection. In CSN-95: Com- puter Science in the Netherlands, pages 62–72, 1995.
[12] Eduardo Bonelli. The polymorphic lambda calculus with explicit substitutions. In International Workshop on Explicit Substitutions: Theory and Applications to