1: \documentclass{article}

2: \usepackage{times}

3: \usepackage[latin1]{inputenc}

4: 

5: \usepackage{pslatex}

6: \usepackage{amsmath}\let\boldsymbol\pmb

7: \usepackage{amssymb}

8: \usepackage{amsfonts}

9: \usepackage{amsthm}

10: \usepackage{hyperref}

11: \usepackage{float}

12: \floatstyle{ruled}

13: \restylefloat{table}

14: \restylefloat{figure}

15: \def\topfraction{0.77}

16: 

17: \usepackage{color}

18: \newcommand{\p}{{\sf P}}

19: \newcommand{\cJ}{{\cal J}}

20: \newcommand{\gO}{\Delta\Delta}

21: \newcommand{\spazio}{${}$\ \ }

22: \newcommand{\ctasprimo}{\vdash^{\tytv'}}

23: \newcommand{\filterscheme}{{\cal S}}

24: \newtheorem{fact}{Fact}[section]

25: \newenvironment{notation}{\paragraph{{\bf Notation.}}}{}

26: \newtheorem{proposition}[fact]{Proposition}

27: \newtheorem{remark}[fact]{Remark}

28: \newtheorem{lemma}[fact]{Lemma}

29: \newtheorem{corollary}[fact]{Corollary}

30: \newtheorem{definition}[fact]{Definition}

31: \newtheorem{theorem}[fact]{Theorem}

32: \newcommand{\Ruled}[2]{\mbox{$\displaystyle\frac{#1}{#2}$}}

33: \newcommand{\md}{}

34: \newcommand{\DK}{DD}

35: \newcommand{\KKD}{KD}

36: \newcommand{\ncomment}[1]{{\sf Comment:} #1}

37: \newcommand{\forget}[1]{}

38: \newtheorem{exercise}{Exercise}

39: 

40: \newcommand{\napp}[3]{[#3]^{#2}_{#1}}

41: \newcommand{\ncomp}[3]{\dlsqb{#3}\drsqb^{#2}_{#1}}

42: \newcommand{\ffun}{{\sf fun}}

43: \newcommand{\true}{{\sf true}}

44: \newcommand{\orn}{{\sf or}}

45: \newcommand{\Nsf}{\mbox{\sf N}}

46: \newcommand{\mmpp}{\mbox{\sf pp}}

47: \newcommand{\mapp}{\mbox{\sf pp}}

48: \newcommand{\oopp}{\mbox{\sf p}}

49: \newcommand{\io}{\mbox{\sf i}_0}

50: \newcommand{\jo}{\mbox{\sf j}_0}

51: \newcommand{\inn}{\mbox{\sf i}_n}

52: \newcommand{\jn}{\mbox{\sf j}_n}

53: \newcommand{\im}{\mbox{\sf i}_m}

54: \newcommand{\jmmd}{\mbox{\sf j}_{m-2}}

55: \newcommand{\inmu}{\mbox{\sf i}_{n-1}}

56: \newcommand{\jnmu}{\mbox{\sf j}_{n-1}}

57: \newcommand{\impu}{\mbox{\sf i}_{m+1}}

58: \newcommand{\jmmu}{\mbox{\sf j}_{m-1}}

59: 

60: %n+1-symbols

61: \newcommand{\set}[1]{\{#1\}}

62: \newlength{\lrulenamec}

63: \setlength{\lrulenamec}{5mm}

64: %\rulec{a}{b}{c} = a b/c

65: \newcommand{\rulec}[3]

66: {\makebox[\lrulenamec]{#1\enskip \enskip\enskip} $\displaystyle

67: \frac{#2}{#3}$}

68: \newcommand{\ruled}[2]{\mbox{$\displaystyle\frac{#1}{#2}$}}

69: \newcommand {\axiomc}[2]

70: {\makebox[\lrulenamec]{#1\enskip\enskip\enskip} $#2$}

71: 

72: %0-symbols

73: 

74: %general

75: %\newcommand{\imp} {\Rightarrow}

76: \newcommand{\impl} {\Leftarrow}

77: \newcommand{\bred} {\longrightarrow_\beta}

78: \newcommand{\ered} {\longrightarrow_\eta}

79: 

80: 

81: %set of types

82: \newcommand{\sitb}[2]{{\bf \Pi}^{#2}_{#1}}

83: \newcommand{\into} {\cap}

84: \newcommand{\ti}{\lambda\into^{\tytv}}

85: \newcommand{\tin}{{\ti}_{{\cal B}}}

86: \newcommand{\tityt}{\lambda\into^{\tytv}_{\tyt}}

87: \newcommand{\titnu}{{\ti}_{\tnu}}

88: \newcommand{\varv} {{\sf V}\!\!{\sf V}}

89: \newcommand{\varvvar} {\varv_{\vvar}}

90: \newcommand{\con}{{{\sf C}\!\!\!\!{\sf C}}}

91: \newcommand{\convcon}{\con_{\vcon}}

92: \newcommand{\sit} {\type(\ti(\varv,\con))}

93: \newcommand{\sita} {{\type}}

94: %\newcommand{\arr} {\rightarrow}

95: \newcommand{\tyt} {\Omega}

96: \newcommand{\tnu} {\nu}

97: \newcommand{\tb} {\chi}

98: \newcommand{\tf} {\varphi}

99: \newcommand{\vari} {\varv_{\infty}}

100: \newcommand{\vare} {\varv_{\emptyset}}

101: \newcommand{\cone} {\con_{\emptyset}}

102: \newcommand{\contnu} {\con_{\tnu}}

103: \newcommand{\cont} {\con_{\tyt}}

104: \newcommand{\conb} {\con_{\tb}}

105: \newcommand{\conf} {\con_{\tf}}

106: \newcommand{\cons} {\con_{\star}}

107: \newcommand{\vvar} {\diamond}

108: \newcommand{\vcon} {\circ}

109: \newcommand{\conv}{\con^{\tytv}}

110: %\newcommand{\varv} {V}_{\vvar}}

111: \newcommand{\vars} {V_{\star}}

112: \newcommand{\sitv} {\type(\varv,\con)}

113: \newcommand{\sitvtytv}{\type^{\tytv}}

114: 

115: \newcommand{\siitvc}{\type_\vcon}

116: \newcommand{\siitv}{\type}

117: \newcommand{\siiitv}{\type(\ti(\varv,\con))}

118: \newcommand{\sitva} {{\bf \Pi}(\ti,V_{\vvar},\con_{\vcon})}

119: \newcommand{\tva} {A}

120: \newcommand{\tvb} {B}

121: \newcommand{\tvc} {C}

122: \newcommand{\tvcv} {\psi}

123: \newcommand{\tvav} {\psi}

124: \newcommand{\tvd} {D}

125: \newcommand{\tve} {E}

126: \newcommand{\tvf} {F}

127: \newcommand{\tvg} {G}

128: \newcommand{\tvh} {H}

129: \newcommand{\tvi} {I}

130: \newcommand{\tvj} {J}

131: \newcommand{\tvk} {K}

132: \newcommand{\tvl} {L}

133: \newcommand{\tvm} {M}

134: \newcommand{\tvn} {N}

135: \newcommand{\tvp} {P}

136: \newcommand{\tvo} {O}

137: \newcommand{\tvq} {Q}

138: \newcommand{\tvr} {R}

139: \newcommand{\tvs} {S}

140: \newcommand{\tvt} {T}

141: \newcommand{\tvu} {U}

142: \newcommand{\tvv} {V}

143: \newcommand{\tvx} {X}

144: \newcommand{\tvy} {Y}

145: \newcommand{\tvw} {W}

146: \newcommand{\tvz} {Z}

147: \newcommand{\tvalpha} {\alpha}

148: \newcommand{\tvbeta} {\beta}

149: \newcommand{\tvxi}{\xi}

150: %bases

151: %\newcommand{\bbases}{{\sf B}_{\vvar\vcon}}

152: \newcommand{\bbases}{{\sf B}(\sitvtytv)}

153: %\newcommand{\ttypesystems}{{\sf T}^\tytv_{\vvar\vcon}}

154: \newcommand{\ttypesystems}{{\sf T}^\tytv}

155: %order on types

156: \newcommand{\sar}[1]{\Sigma^{#1}}

157: \newcommand{\tleq} {\leq}

158: \newcommand{\tleqt}{\tleq_{\tytv}}

159: \newcommand{\nottleq}{\mbox{$\not\tleq$}}

160: \newcommand{\nottleqt}{\mbox{$\not\tleq$}_\tytv}

161: \newcommand{\nottleqs}{\mbox{$\not\tleqs$}}

162: \newcommand{\tleqinfty}{\tleq_{\infty}}

163: \newcommand{\teqinfty}{\sim_{\infty}}

164: \newcommand{\nottleqinfty}{\mbox{$\not\tleq$}_\infty}

165: \newcommand{\teql}{\sim_{{\abo}}}

166: \newcommand{\notteql}{\mbox{$\not\sim$}_{\abo}}

167: \newcommand{\binto} {\bigcap}

168: %\renewcommand{\teq} {\sim}

169: \newcommand{\teqt}{{}{\sim_{\tytv}}}

170: \newcommand{\notteqt}{{}{\mbox{$\not\sim$}_{\tytv}}}

171: %\newcommand{\notteqt}{\mbox{$\not\teq$}_\tytv}

172: \newcommand{\tleqs}{\tleq_\star}

173: \newcommand{\tleqp}{\tleq_{\park}}

174: \newcommand{\teqp}{\sim_{\park}}

175: \newcommand{\nottleqp}{\mbox{$\not\tleq$}_{\oopp}}

176: \newcommand{\teqpp}{\sim_{\oopp}}

177: \newcommand{\tytv} {\bigtriangledown}

178: \newcommand{\calT} {\sar{\tytv}}

179: \newcommand{\calS}{\cal S}

180: \newcommand{\calTs}{{\cal T}}

181: 

182: %type assignment

183: 

184: \newcommand{\ctas}{\vdash^\tytv}

185: \newcommand{\ctastyt}{\vdash^\tytv_\tyt}

186: \newcommand{\ctastnu}{\vdash^\tytv_\tnu}

187: %\newcommand{\rtas} {\vdash^{\tytv R}_{\vvar\vcon}}

188: \newcommand{\rtas}{\vdash^{\tytv R}}

189: \newcommand{\ax} {\mbox{Ax}}

190: \newcommand{\axtyt} {\mbox{Ax-$\tyt$}}

191: \newcommand{\axtnu}{\mbox{Ax-$\tnu$}}

192: \newcommand{\arrI} {\arr  \mbox{\rm I}}

193: \newcommand{\arL} {\arr  \mbox{\rm L}}

194: \newcommand{\arR} {\arr  \mbox{\rm R}}

195: \newcommand{\intoL} {\into \mbox{\rm L}}

196: \newcommand{\intoR}{\into\mbox{\rm R}}

197: \newcommand{\intI} {\into \mbox{\rm I}}

198: \newcommand{\arE} {\arr  \mbox{\rm E}}

199: \newcommand{\rleq} {\tleqt}

200: \newcommand{\rlet} {\tleq}

201: \newcommand{\lleq} {\tleqt\mbox{\rm L}}

202: \newcommand{\axr} {\mbox{Ax$_R$}}

203: \newcommand{\axtytr} {\mbox{Ax-$\tyt_R$}}

204: \newcommand{\axnur} {\mbox{Ax-$\tnu_R$}}

205: \newcommand{\intIr} {\into \mbox{\rm I}_R}

206: \newcommand{\arEr} {\arr  \mbox{\rm E}_R}

207: \newcommand{\arIr} {\arr \mbox{\rm I}_R}

208: \newcommand{\req} {\teq}

209: \newcommand{\ub} {\uplus}

210: \newcommand{\ob}

211: {\subseteq\!\!\!\!\!\raisebox{1.75pt}{\mbox{\tiny +}}\,}

212: \newcommand{\rob}

213: {\mbox{$\supseteq\!\!\!\!\!\!\raisebox{1.75pt}{\mbox{\tiny

214: +}}\,\,\,$}}

215: %\newcommand{\ctav}{\vdash^\emptyset_{\vvar\vcon}}

216: \newcommand{\ctav}{\vdash^{\code}}

217: \newcommand{\ctavn}{\ctav_{{\cal B}}}

218: %\newcommand{\ctae}{\vdash^\eta_{\vvar\vcon}}

219: \newcommand{\ctae}{\vdash^{\bake}}

220: \newcommand{\ctaen}{\ctae_{{\cal B}}}

221: \newcommand{\ctaf}{\vdash^{\cdz}_{\tyt}}

222: \newcommand{\ctal}{\vdash^{\abo}_{\tyt}}

223: \newcommand{\ctanu}{\vdash^{\ehr}}

224: \newcommand{\cts}{\vdash^{\star}}

225: \newcommand{\tasP}{\vdash^{\park}_{\tyt}}

226: \newcommand{\intE} {\into \mbox{\rm E}}

227: \newcommand{\reta} {\mbox{$R$-$\eta$}}

228: \newcommand{\calD} {{\cal D}}

229: %%      \prooftree

230: %%              hyp1            produces:

231: %%              hyp2

232: %%              hyp3                    hyp1    hyp2    hyp3

233: %%      \justifies              -------------------- rulename

234: %%              concl                              concl

235: %%      \thickness=0.08em

236: %%      \shiftright 2em

237: %%      \using

238: %%              rulename

239: %%      \endprooftree

240: \def\intItp{\using(\intI)\thickness.08em\justifies}

241: \def\intIrtp{\using(\intIr)\thickness.08em\justifies}

242: \def\rleqtp{\using(\rleq)\thickness.08em\justifies}

243: \def\arItp{\using(\arrI)\thickness.08em\justifies}

244: \def\arIrtp{\using(\arIr)\thickness.08em\justifies}

245: \def\arEtp{\using(\arE)\thickness.08em\justifies}

246: \def\arErtp{\using(\arEr)\thickness.08em\justifies}

247: \def\arLtp{\using(\arL)\thickness.08em\justifies}

248: \def\arRtp{\using(\arR)\thickness.08em\justifies}

249: \def\rleqt{\using\rleq\thickness.08em\justifies}

250: \def\arIt{\using\arrI\thickness.08em\justifies}

251: \def\arEt{\using\arE\thickness.08em\justifies}

252: 

253: 

254: 

255: %computability

256: %\newcommand{\ccomp}{\mbox{\it Comp}^\tytv_{\vvar\vcon}}

257: \newcommand{\ccomp}{\mbox{\it Comp}^\tytv}

258: \newcommand{\anf} {P}

259: \newcommand{\lred} {\longrightarrow_l}

260: \newcommand{\mis} {{\#}}

261: \newcommand{\vapp} {\dagger}

262: \newcommand{\aset} {{\cal A}_{\tytv}}

263: \newcommand{\asetc} {{\cal A}_{\park}}

264: \newcommand{\axphi} {\mbox{Ax-$\Phi$}}

265: \newcommand {\app} {\mbox{$\cal A$}_\tytv}

266: \newcommand{\appa} {\mbox{$\cal A$}_\alpha}

267: \newcommand{\appb} {\mbox{$\cal A$}_{\abo}}

268: \newcommand{\appc} {\mbox{$\cal A$}_{\park}}

269: \newcommand {\apps} {\mbox{$\cal A$}_{\sco}}

270: \newcommand{\appf} {\mbox{$\cal A$}_{\cdz}}

271: \newcommand{\acomp}{\mbox{\it Comp}_{\tytv}}

272: \newcommand{\acompa}{\mbox{\it Comp}_{\tytv}}

273: \newcommand{\acompf}{\mbox{\it Comp}_{\cdz}}

274: \newcommand{\acompb}{\mbox{\it Comp}_{\abo}}

275: \newcommand{\acompc}{\mbox{\it Comp}_{\park}}

276: \newcommand{\acompP}{\mbox{\it Comp}^{\park}}

277: \newcommand{\tasS}{\vdash^{\sco}}

278: \newcommand{\tleql}{\tleq_{\abo}}

279: \newcommand{\acompl}{\acompb}

280: 

281: 

282: %filters

283: %characterization

284: \newcommand{\FX} {X}

285: \newcommand{\FY} {Y}

286: %\newcommand{\SF}{{\cal F}^\tytv_{\vvar\vcon}}

287: \newcommand{\SF}{{{\cal F}^\tytv}}

288: \newcommand{\FFF}[1]{\uparrow^{#1}}

289: \newcommand{\D} {{\cal D}}

290: \newcommand{\fcD} {[\D\arr \D]}

291: \newcommand{\ela} {a}

292: \newcommand{\elb} {b}

293: \newcommand{\elc} {c}

294: \newcommand{\ele} {e}

295: \newcommand{\step}[2] {#1\Rightarrow#2}

296: \newcommand{\el} {d}

297: \newcommand{\Dleq} {\sqsubseteq}

298: \newcommand{\Dgeq} {\sqsupseteq}

299: \newcommand{\Dsup} {\sqcup}

300: \newcommand{\Dinf} {\sqcap}

301: \newcommand{\DInf} {\sqcap}

302: \newcommand{\DSup} {\bigsqcup}

303: \newcommand{\mmm} {{\sf m}}

304: \newcommand{\env} {{\sf Env}}

305: \newcommand{\En}{{{\sf Em}}}

306: \newcommand{\G}{\Gamma}

307: \newcommand{\End}{{\cal E}}

308: \newcommand{\en} {\rho}

309: \newcommand{\ag} {\models}

310: \newcommand{\dlsqb}{[\![}

311: \newcommand{\drsqb}{]\!]}

312: \newcommand{\interpretation}[3]{\dlsqb{#1}\drsqb^{#3}_{#2}}

313: \newcommand{\intstyt}[2]{\dlsqb{#1}\drsqb^{\tyt}_{#2}}

314: \newcommand{\ints}[2]{\dlsqb{#1}\drsqb^{\tytv}_{#2}}

315: \newcommand{\intsstar}[2]{\dlsqb{#1}\drsqb^{\star}_{#2}}

316: \newcommand{\intsp}[2]{\dlsqb{#1}\drsqb^{\oopp}_{#2}}

317: \newcommand{\intsinfty}[2]{\dlsqb{#1}\drsqb^\infty_{#2}}

318: %\newcommand{\ints}[2]{\dlsqb{#1}\drsqb_{#2}}

319: %\newcommand{\fun} {F^\tytv_{\vvar\vcon}}

320: \newcommand{\fun}{F^\tytv}

321: \newcommand{\funs}{F}

322: %\newcommand{\gr} {G^\tytv_{\vvar\vcon}}

323: \newcommand{\gr}{G^\tytv}

324: \newcommand{\grs}{G}

325: \newcommand{\three}[3]{\langle {#1},{#2},{#3} \rangle}

326: \newcommand{\two}[2]{\langle {#1},{#2} \rangle}

327: \newcommand{\Dfun} {F_\D}

328: \newcommand{\Dgr} {G_\D}

329: \newcommand{\KD} {{\cal K}(\D)}

330: %\newcommand{\calTss} {{\calTs_\star_{\emptyset\star}}}

331: \newcommand{\calTss}{\calTs_\star}

332: \newcommand{\calTsomega}{\calTs_{\SM}}

333: \newcommand{\calTsplotkin}{\calTs_{\PM}}

334: \newcommand{\calTsengeler}{\calTs_{\En}}

335: 

336: 

337: %completeness

338: \newcommand{\intm}[2]{\dlsqb{#1}\drsqb^{\M}_{#2}}

339: \newcommand{\tenv} {{\sf TE}}

340: \newcommand{\ten} {{\cal V}}

341: \newcommand{\M} {{\cal M}}

342: \newcommand{\agv} {\ag^{\tytv}}

343: \newcommand{\coni} {\con_\infty}

344: 

345: %Information Systems

346: %\newcommand{\A}{{\cal A}}

347: \newcommand{\four}[4] {\langle {#1},{#2},{#3},{#4} \rangle}

348: 

349: %Other Models

350: \newcommand{\SM}{{\sf P}(\omega)}

351: \newcommand{\SMM}{{\nabla}(\omega)}

352: \newcommand{\PM} {{\sf Pm}}

353: \newcommand{\Pat} {\phi}

354: %\newcommand{\E} {{\cal C}}

355: \newcommand{\AtE} {{\con_\infty}}

356: \newcommand{\intsc}[2]{\dlsqb{#1}\drsqb^{{\sf P}(\omega)}_{#2}}

357: \newcommand{\intP}[2]{\dlsqb{#1}\drsqb^{\PM}_{#2}}

358: \newcommand{\intEM}[2]{\dlsqb{#1}\drsqb^{\En}_{#2}}

359: \newcommand{\intl}[2]{\dlsqb{#1}\drsqb^{\abo}_{#2}}

360: \newcommand{\intv}[2]{\dlsqb{#1}\drsqb^v_{#2}}

361: \newcommand{\intnu}[2]{\dlsqb{#1}\drsqb^\tnu_{#2}}

362: \newcommand{\redstar}{\stackrel{*}{\longrightarrow}}

363: \newcommand{\Q} {{\cal Q}}

364: \newcommand{\qel} {q}

365: \newcommand{\qelp} {p}

366: \newcommand{\qelr} {r}

367: \newcommand{\qat} {a}

368: \newcommand{\sleq} {\sqsubseteq_s}

369: \newcommand{\Qfun} {F_\Q}

370: \newcommand{\Qgr} {G_\Q}

371: \newcommand{\cp}  {\mbox{\it Con}}

372: \newcommand{\ncp} {\mbox{$\overline{\cp}$}}

373: \newcommand{\AQ} {\mid\Q\mid}

374: 

375: 

376: 

377: %\newcommand{} {}

378: %\newcommand{} {}

379: %\newcommand{} {}

380: %\newcommand{} {}

381: 

382: 

383: \newcommand\type{{\sf T\!\!\!\!\!T}}

384: \newcommand{\arr}{\rightarrow}

385: \renewcommand\qed{~\rule{2mm}{2mm}}

386: \newcommand\qedf{\mbox{$\qed$}}

387: \newcommand\wit[1]{\rule{#1mm}{0mm}}

388: \newcommand\hoog[1]{\rule{0mm}{#1}}

389: 

390: \newcommand{\semic}{\! : \!}

391: \newcommand{\doppiolambda}{\lambda\!\!\lambda}

392: \newcommand{\naturali}{\mbox{\rm I$\!$N}}

393: \newcommand{\tleqtomega}{\tleq_{\tytv''}}

394: \newcommand{\tsimtomega}{\sim_{\tytv''}}

395: \newcommand{\ctassecondo}{{\vdash^{\tytv''}}}

396: \newcommand{\ugualesintattico}{\equiv}

397: \newcommand{\ctastas}{\ctas}

398: \newcommand{\tipom}{W}

399: \newcommand{\FV}{\mbox{FV}}

400: \newcommand{\typetytv}{\type^{\tytv}}

401: \newcommand{\tM}{{\sf t}}

402: \newcommand{\tN}{{\sf u}}

403: \newcommand{\tE}{{\sf e}}

404: 

405: 

406: 

407: \begin{document}

408: 

409: \title{Intersection Types and Lambda Theories

410: \thanks{Partially supported by MURST Cofin'00 AITCFA  Project, MURST

411: Cofin'01 COMETA Project, and by  EU within the FET - Global Computing initiative, project DART IST-2001-33477.} }

412: \author{

413: M.Dezani-Ciancaglini\thanks{Dipartimento di Informatica, Universit\`a di Torino, Corso

414: Svizzera 185, 10149 Torino, Italy  {\tt dezani@di.unito.it}}

415: \and S.Lusin

416: \thanks{Dipartimento di Informatica, Universit\`a di Venezia,

417: {via Torino 153, 30170 Venezia, Italy}  {\tt slusin@oink.dsi.unive.it}}}

418: \date{}

419: \maketitle

420: 

421: 

422: \begin{abstract}

423: We illustrate the use of intersection types as a semantic tool for

424: showing properties of the lattice of $\lambda$-theories.  Relying

425: on the notion of {\em easy intersection type theory} we

426: successfully build a filter model in which  the

427: interpretation of an arbitrary simple easy term is any filter which can be described in an uniform way by a predicate. This allows us to prove the consistency of a

428: well-know $\lambda$-theory: this consistency has interesting consequences on the algebraic structure of the lattice of $\lambda$-theories.

429: \end{abstract}

430: 

431: \section*{Introduction}

432: 

433: Intersection types were introduced in the late 70's by Dezani and

434: Coppo \cite{coppdeza80,coppdezavenn80,barecoppdeza83}, to overcome

435: the limitations of Curry's type discipline. They are a very

436: expressive type language which allows to describe and capture

437: various properties of $\lambda$-terms. For instance, they have

438: been used in \cite{pott80}

439:  to give the first type theoretic characterization of {\em strongly

440:  normalizable} terms and in \cite{coppdezazacc87}  to

441:  capture {\em persistently normalizing terms} $\md$ and {\em

442:  normalizing terms}$\md$. See \cite{dezahonsmoto2000} for a more

443: complete account of this line of research.

444: 

445: Intersection types have a very significant realizability semantics

446: with respect to applicative structures. This is a generalization

447: of Scott's natural semantics \cite{scot72} of simple types.

448: According to this interpretation types denote subsets of the

449: applicative structure, an arrow type $A\to B$ denotes the sets of

450: points which map all points belonging to the interpretation of $A$

451: to points belonging to the interpretation of $B$, and an

452: intersection type $A\into B$ denotes the intersections of the

453: interpretation of $A$ and the interpretation of $B$. Building on

454: this, intersection types have been used in \cite{barecoppdeza83}

455: to give a proof of the completeness of the natural semantics of

456: Curry's simple type assignment system in applicative structures,

457: introduced in \cite{scot72}.

458: 

459: Intersection types have also an alternative semantics based on

460: {\em duality} which is related to Abramsky's {\em Domain Theory in

461: Logical Form } \cite{abra91}. Actually it amounts to the

462: application of that  paradigm to the special case of

463: $\omega$-algebraic complete lattice models of pure

464: $\lambda$-calculus, \cite{coppdezahonslong84}.  Namely, types correspond to

465: {\em compact elements}: the type $\Omega$ denoting  the least

466: element, intersections denoting {\em joins}  of compact elements,

467: and arrow types denoting {\em step functions} of compact elements.

468: A typing judgment then can be interpreted as saying that a given

469: term belongs to a pointed compact open set in a $\omega$-algebraic

470: complete lattice model of $\lambda$-calculus. By duality, type

471: theories give rise to {\em filter $\lambda$-models}. Intersection

472: type assignment systems can then be viewed as {\em finitary

473: logical} descriptions of the interpretation of $\lambda$-terms in

474: such models, where the meaning of a $\lambda$-term is the set of

475: types which are deducible for it.

476: This duality lies at the heart of the success of intersection

477: types as a powerful tool for the analysis of $\lambda$-models, see

478: \cite{plot93} and the references there.

479: 

480: A key observation is that the $\lambda$-models we build out of intersection types

481: differ only for the {\em preorder relations} between types. Changing

482: these preorders in fact allow us to give different

483: interpretations to $\lambda$-terms. In all these preorders crucial are the

484: equivalences between atomic types and intersections of arrow types: therefore

485: {\em type isomorphisms} are the corner stones of filter model constructions.

486: 

487: In \cite{aleslusi02} Alessi and Lusin faced the issue of easiness

488: proofs of $\lambda$-terms from the semantic point of view (we

489: recall that a closed term $\tE$ is {\em easy} if, for any other

490: closed term $\tM$, the theory $\lambda\beta + \{\tM=\tE\}$ is

491: consistent). Actually the mainstream of easiness proofs is based

492: on the use of syntactic tools (see \cite{kupe97} and the

493: references there). Instead, very little literature can be found on

494: easiness issues handled by semantic tools, we can mention the

495: papers \cite{zylb91}, \cite{baetboer79},  \cite{alesdezahons01},

496: \cite{aleslusi02}.

497: 

498: 

499: Going in the direction of \cite{alesdezahons01}, in

500: \cite{aleslusi02} Alessi and Lusin introduced the notion of {\em

501: simple easiness}: roughly speaking, an unsolvable term $\tE$ is

502: simple easy if, for each filter model ${\cal F}^{\tytv}$ built on

503: an easy intersection type theory $\Sigma^{\tytv}$, any type $Z$ in

504: $\Sigma^{\tytv}$, we can expand $\Sigma^{\tytv}$ to a new easy

505: intersection type theory $\Sigma^{\tytv'}$ such that the

506: interpretation of $\tE$ in ${\cal F}^{\tytv'}$ is the sup of the old

507: interpretation of $\tE$ in ${\cal F}^{\tytv}$ and of the filter

508: generated by $Z$.

509: 

510: 

511: A consequence is that simple easiness is a stronger notion than

512: easiness. A simple easy term $\tE$ is easy, since, given an

513: arbitrary closed term $\tM$, it is possible to build (in a canonical

514: way) a non-trivial filter model which equates the interpretation

515: of $\tE$ and $\tM$.

516: 

517: Besides of that, simple easiness is interesting in itself, since

518: it has to do with minimal sets of axioms which are needed in order

519: to give the easy terms certain types. This can be put at work to interpret

520: easy terms by filters which can be described in an uniform way by predicates.

521: 

522: 

523: Building on the duality between type intersections and joins, arrows and step functions, given an arbitrary simple easy term we build a $\lambda$-model in which this term is interpreted as the join. 

524: In this way we can prove the consistency of an interesting $\lambda$-theory. This consistency has been used in \cite{lusisali02} to show that there exists a sublattice of the lattice of $\lambda$-theories

525: which satisfies a restricted form of distributivity, called meet

526: semidistributivity,

527: and a nontrivial congruence identity (i.e., an identity in the language

528: of lattices enriched by the relative product of binary relations).

529: 

530: 

531: The present paper is organized as follows. In

532: Section~\ref{theories} we present easy intersection type theories

533: and type assignment systems for them. In

534: Section~\ref{filter-models} we introduce $\lambda$-models based on

535: spaces of filters in easy intersection type theories. Section

536: \ref{section-simple-easy-terms} gives the main contribution of the present paper: each simple easy term can be interpreted as an arbitrary filter which can be described in an uniform way by a predicate. Finally in Section \ref{appl} we apply our result to show the consistency of a $\lambda$-theory which has interesting consequences on the algebraic properties of the lattice of $\lambda$-theories.

537: 

538: \section{Intersection Type Assignment

539: Systems}\label{intersecion-type-intro} \label{theories} {\em

540: Intersection types} are syntactical objects built inductively by

541: closing a given set $\con$ of {\em type atoms} (constants) which

542: contains the universal type $\tyt$ under the {\em function type}

543: constructor $\arr$ and the {\em intersection} type constructor

544: $\into$.

545: \begin{definition}[Intersection Type Language]$\;$\\

546: Let $\con$ be a countable set of constants such that

547: $\tyt\in\con$. The {\em intersection type language} over $\con$,

548: denoted by

549:   $\type=\type(\con)$ is defined by the following

550: abstract syntax:

551:  \[

552: \type = \con \mid \type \arr  \type \mid \type \into \type.

553: \]

554: \end{definition}

555: Notice that the most general form of an intersection type is a

556: finite intersection of arrow types and type constants.

557: \smallskip

558: 

559: \noindent

560: {\bf Notation} Upper case Roman letters i.e.\

561: $\tva,\tvb,\ldots$, will denote

562:   arbitrary types. Greek letters will denote constants in $\con$.

563:     When writing intersection types we shall use the

564:   following convention: the constructor $\into$ takes precedence over

565:   the constructor $\arr $ and it associates to the right. \smallskip

566: 

567: \noindent Much of the expressive power of intersection type

568: disciplines comes from the fact that types can be endowed with a

569: {\em preorder relation} $\leq$, which induces the structure of a

570: meet semi-lattice with respect to $\into$, the top element being

571: $\tyt$. We recall here the notion of {\em easy\/} intersection type

572: theory as first introduced in \cite{aleslusi02}.

573: 

574: 

575: \begin{definition}[Easy intersection type

576: theories]\label{intersection-type-theories}$\;$\\ Let

577: $\type=\type(\con)$ be an intersection type language. The {\em

578: easy intersection type theory\/} ({\em eitt} for short)

579: $\Sigma(\con,{\tytv})$ over $\type$ is the set of all judgments

580: $\tva\tleq\tvb$ derivable from $\tytv$, where $\tytv$ is a

581: collection of axioms and rules such that (we write $A\sim B$ for

582: $A\tleq B \;\&\; B\tleq A$):

583: \begin{enumerate}

584: \item $\tytv$ contains the

585:  set $\overline{\tytv}$ of axioms and rules:

586:  $$\begin{array}[b]{rlrl}

587:  \mbox{(refl)}&\tva\tleq\tva

588:  &\mbox{(idem)}&\tva\tleq\tva\into\tva\\[0.5em]

589: \mbox{(incl$_L$)}& \tva \into \tvb \tleq \tva &\mbox{(incl$_R$)}&

590: \tva \into \tvb \tleq \tvb\\[0.5em] \mbox{(mon)}&\ruled{ \tva

591: \tleq \tva'\;\;\; \tvb \tleq \tvb'}{

592:                      \tva \into \tvb \tleq \tva' \into \tvb'}

593: &\mbox{(trans)}&\ruled{ \tva \tleq \tvb\;\;\; \tvb \tleq \tvc}{

594:                      \tva \tleq \tvc}\\[1em]

595: \mbox{($\tyt$)}&\tva\tleq\tyt &\mbox{($\tyt$-$\eta$)} &

596: \tyt\tleq\tyt\to\tyt\\[0.5em] \mbox{($\to$-$\into$)} & (A\to

597: B)\into(A\to C)\tleq A\to B\into C &\mbox{($\eta$)} &\ruled{

598: A'\tleq A\;\;\; B\tleq B'}{ A\to B \tleq A'\to B'}

599: \end{array}$$

600: \item

601: further axioms can be of the following two shapes only:

602: \[\begin{array}{l}

603: \psi\tleq\psi',\\ \psi\sim\binto_{h\in H} (\xi_{h}\rightarrow

604: E_{h}).

605: \end{array}\]

606: where $\psi,\psi',\xi_{h}\in \con$, $E_{h}\in\type$, and

607:  $\psi,\psi'\not\equiv\tyt$;

608:  \item $\tytv$ does not contain further rules;

609: \item

610: for each $\psi\not\equiv\tyt$ there is exactly one axiom in

611: $\tytv$ of the shape $\psi\sim A$;

612: \item

613: let $\tytv$ contain $\psi\sim \binto_{h\in H} (\xi_{h}\rightarrow

614: E_{h})$ and $\psi'\sim \binto_{k\in K} (\xi'_{k}\rightarrow

615: {E'}_{k})$. Then $\tytv$ contains also $\psi\tleq\psi'$ iff for

616: each $k\in K$, there exists $h_{k}\in H$ such that ${\xi'}_{k}\leq

617: \xi_{h_{k}}$ and $E_{h_{k}}\leq {E'}_{k}$ are both in $\tytv$.

618: %$\;$

619: \end{enumerate}

620: \end{definition}

621: %\vspace{.2in}

622:  \noindent Notice that:\\ (a) since

623: $\tyt\sim\tyt\to\tyt\in\Sigma(\con,{\tytv})$ by  ($\tyt$) and

624: ($\tyt$-$\eta$), it follows that all atoms in $\con$  are

625: equivalent to suitable (intersections of) arrow types;\\  (b)

626: $\into$ (modulo $\sim$) is associative and commutative;\\ (c) in

627: the last clause of the above definition $E'_k$ and $E_{h_k}$ must

628: be constant types for each $k\in K$.

629: \smallskip

630: 

631: \noindent

632: {\bf Notation} When we consider an eitt

633: $\Sigma(\con,{\tytv})$, we will write $\conv$ for $\con$,

634: $\type^{\tytv}$ for $\type(\con)$ and $\sar{\tytv}$ for

635: $\Sigma(\con,\tytv)$. Moreover  $\tva\tleqt\tvb$ will be short for

636:   $(\tva\tleq\tvb)\in\sar{\tytv}$ and $A\teqt B$ for $

637:   A\tleqt B\tleqt A$.

638:   We will consider syntactic equivalence ``$\equiv $''  of types

639:   up to associativity

640: and commutativity of $\into$. \\

641: 

642: A nice feature of eitts is that the order between intersections of arrows  agrees with the order between joins of step functions. This is stated in the following theorem, whose proof can be found in \cite{aleslusi02}.

643: 

644: \begin{theorem}\label{strong-beta-are-beta}$\;$\\

645: For all $I$, and $\tva_i, \tvb_i, \tvc, \tvd \in \type^{\tytv}$,

646: \[

647: \binto_{i \in I}(\tva_i \arr  \tvb_i)\tleqt \tvc \arr  \tvd

648: \;\Rightarrow\;\exists J \subseteq I. \tvc \tleqt \binto_{i \in

649: J}\tva_i\;\&\;\binto_{i \in J}\tvb_i\tleqt  \tvd,\] provided that

650: $\tvd\notteqt\tyt$.

651:     \end{theorem}

652: 

653: Before giving the crucial notion of {\em intersection-type

654: assignment system}, we introduce bases and some related

655: definitions.

656: \begin{definition}[Bases]\label{definition-for-type-assignment}$\;$

657: \begin{enumerate}

658: \item

659:  A ${\tytv}$-{\em basis} is a (possibly infinite) set

660:   of statements of the shape $x\semic\tva$, where $\tva\in\type^{\tytv}$,

661:   with all variables distinct.

662:   \item

663:   If $\Gamma$ is a ${\tytv}$-{basis}

664:   and $\tva\in\type^{\tytv}$ then

665:  $\Gamma,x\semic A$ is short for $\Gamma\cup\{x\semic A\}$ when $x\notin\Gamma$.

666: \end{enumerate}

667: \end{definition}

668: \begin{definition}[The type assignment system]\label{typeass}$\;$\\

669:    The {\em intersection type

670:     assignment system}\ relative to the eitt $\sar{\tytv}$, notation

671:   ${\ti}$, is a formal system for deriving judgements of the

672:   form $\Gamma \ctas \tM:\tva$, where

673:   the {\em subject\/} $\tM$ is an untyped $\lambda$-term,

674:   the {\em predicate\/} $\tva$ is  in $\type^{\tytv}$,

675:   and $\Gamma$ is a ${\tytv}$-basis.

676: Its axioms and rules are the following:

677: \[\begin{array}{rlrl}

678:  (\ax) & \Ruled{(x\semic\tva)\in\Gamma}{\Gamma \ctas x\semic\tva} &(\axtyt) &  \Gamma \ctas

679: \tM:\tyt\\[1em]

680:  (\arrI ) & \Ruled{\Gamma, x\semic\tva\ctas \tM:\tvb}{\Gamma \ctas \lambda x.\tM:\tva\arr

681: \tvb} & (\arE) & \Ruled{\Gamma \ctas

682: \tM:\tva\rightarrow\tvb\;\;\Gamma \ctas \tN:\tva}{\Gamma \ctas

683: \tM\tN:\tvb} \\[1em] (\intI) & \Ruled{\Gamma \ctas \tM:\tva\;\;\Gamma

684: \ctas \tM:\tvb}{\Gamma \ctas \tM:\tva\into\tvb} & (\tleqt) &  \Ruled

685: {\Gamma \ctas \tM:\tva\;\;\tva\tleqt\tvb}{\Gamma \ctas \tM:\tvb}

686: %

687: \end{array}\]

688: \end{definition}

689: As usual we consider $\lambda$-terms modulo $\alpha$-conversion.

690: Notice that intersection elimination rules $$ (\into E)\ \

691: \ruled{\G \ctas \tM:\tva\into\tvb}{\G \ctas \tM:\tva} \ \ \ \

692: \ruled{\G \ctas \tM:\tva\into\tvb}{\G \ctas \tM:\tvb}$$ can be

693: immediately proved to be derivable in all ${\ti}$.\bigskip

694: 

695: We end this section by stating a Generation Theorem (proved in \cite{aleslusi02}).

696: \begin{theorem}[Generation Theorem]\label{gen-l}$\;$

697: \begin{enumerate}

698: \item \label{gen-l1} Assume $\tva\notteqt\tyt$.

699: $\G\ctas x:\tva$ iff $(x\semic\tvb)\in \G$ and $\tvb\tleqt \tva$

700: for some $\tvb \in \type^{\tytv}$.

701: \item \label{gen-l4}

702: $\G\ctas \tM\tN:\tva$ iff $\G\ctas \tM:\tvb\arr \tva$, and $\G\ctas

703: \tN:\tvb$ for some $\tvb \in \type^{\tytv}$.

704: \item \label{gen-l5}

705: $\G\ctas \lambda x.\tM:\tva$ iff $\G, x\semic\tvb_i\ctas \tM:\tvc_i$

706: and $\binto_{i \in I}(\tvb_i\arr \tvc_i)\tleqt \tva$, for some $I$

707: and $B_i, C_i\in \type^\tytv$.

708: \item \label{gen-l6}

709: $\G\ctas \lambda x.\tM:\tvb \arr \tvc$ iff $\G, x\semic\tvb\ctas

710: \tM:\tvc$.

711: %$\;$

712: \end{enumerate}

713: \end{theorem}

714: 

715: \section{Filter Models}\label{filter-models}

716: In this section we discuss how to  build $\lambda$-models out of

717: type theories. We start with the definition of {\em filter\/} for

718: eitt's. Then we show how to turn the space of filters into an

719: applicative structure. Finally we will define a notion of

720: interpretation of $\lambda$-terms and state that we get

721: $\lambda$-models ({\em filter models}).

722: 

723: Filter models arise naturally in the context of those

724: generalizations of Stone duality that are used in representing

725: domain theory in logical form (see \cite{abra91},

726: \cite{coppdezahonslong84}). This approach provides

727: a conceptually independent semantics to in\-ter\-sec\-tion

728: ty\-pes, the {\em lattice semantics}. Types are viewed as {\em

729: compact elements} of domains. The type $\Omega$ denotes the least

730: element, intersections denote joins of compact elements, and arrow

731: types allow to internalize the space of continuous endomorphisms.

732: Following the paradigm of Stone duality, type theories give rise

733: to filter models, where the interpretation of $\lambda$-terms can

734: be given through a finitary logical description.

735: 

736: \begin{definition}\label{definition-of-filters}$\;$

737:  \begin{enumerate}

738: \item\label{filter1}

739:  A $\tytv$-filter (or a filter over $\typetytv$) is a set

740: $\FX\subseteq \typetytv$ such that:

741: \begin{itemize}

742: \item

743: $\tyt \in \FX$;

744: \item

745: if $\tva \tleqt \tvb$ and $\tva \in \FX$, then $\tvb \in \FX$;

746: \item

747: if $\tva,\tvb \in \FX$, then $\tva\into\tvb \in \FX$;

748: \end{itemize}

749: \item\label{filter2} $\SF$ denotes the set of $\tytv$-filters over

750: $\typetytv$;

751: \item\label{filter3} if $\FX\subseteq \typetytv$,

752: $\FFF{\tytv}\FX$ denotes the $\tytv$-filter generated by $\FX$;

753: \item\label{filter4} a $\tytv$-filter is {\em principal} if it is of the shape $\FFF{\tytv}

754:   \{ \tva\}$, for some type $\tva$. We shall denote $\FFF{\tytv} \{ \tva\}$

755:   simply by $\FFF{\tytv} \tva$.

756: %$\;$

757: \end{enumerate}

758: \end{definition}

759: 

760: It is well known that $\SF$ is an $\omega$-algebraic cpo, whose

761: compact (or finite) elements are the filters of the form $\FFF{\tytv}

762: A$ for some type $A$ and whose bottom element is $\FFF{\tytv}

763: \tyt$.\medskip

764: 

765: Next we endow the space of filters with the notions of application

766: and of $\lambda$-term interpretation. Let ${\sf Env}_\SF$ be the

767: set of all mappings from the set of term variables to $\SF$.

768: 

769: \begin{definition}\label{application}$\;$

770: \begin{enumerate}

771: \item \label{application1}

772: Application $\cdot:\SF\times\SF\rightarrow\SF$  is defined as

773: \[ X\cdot Y =\{ \tvb\mid \exists \tva\in \FY.\tva\to\tvb\in

774: \FX\}.\]

775: \item \label{application2}

776: The interpretation function: $\interpretation{\;}{\;}{\tytv}:

777: \Lambda \times {\sf Env}_\SF \to \SF$ is defined by

778: \[\interpretation{\tM}{\rho}{\tytv} =

779: \{\tva \in \typetytv \mid \exists \Gamma\ag\en.\; \Gamma \ctastas

780: \tM:\tva\},\] where $\rho$ ranges over ${\sf Env}_\SF$ and

781: $\Gamma\ag\en$ if and only $(x\semic \tvb)\in \Gamma$ implies

782: $\tvb\in\en(x)$.

783: \item

784: The triple $\three{\SF}{\cdot}{\interpretation{\;}{\;}{\tytv}}$ is

785: called the {\em filter model} over $\calT$.

786: %$\;$

787: \end{enumerate}

788: \end{definition}

789: 

790: Notice that previous definition is sound, since it is easy to

791: verify that $X\cdot Y$ is a $\tytv$-filter. The key property of ${\cal F}^{\tytv}$ is to be a $\lambda$-model. This is proved in \cite{aleslusi02}.

792: 

793: 

794: 

795: \begin{theorem}\label{strong-beta-implies-lm}$\;$\\

796: The filter model

797: $\three{\SF}{\cdot}{\interpretation{\;}{\;}{\tytv}}$ is a

798: $\lambda$-model, in the sense of Hindley-Longo~\cite{hindlong80},

799: that is:

800: \begin{enumerate}

801: \item\label{hl1}

802: $\interpretation{x}{\rho}{\tytv} = \rho(x)$;

803: \item\label{hl2}

804: $\interpretation{\tM\tN}{\rho}{\tytv} =

805:  \interpretation{\tM}{\rho}{\tytv}\cdot\interpretation{\tN}{\rho}{\tytv}$;

806: \item\label{hl3}

807: $\interpretation{\lambda x.\tM}{\rho}{\tytv}\cdot X =

808: \interpretation{\tM}{\rho[X/x]}{\tytv}$;

809: \item\label{hl4}

810: $(\forall x\in\FV(\tM).\; \interpretation{x}{\rho}{\tytv} =

811: \interpretation{x}{\rho'}{\tytv})\;\Rightarrow\;

812: \interpretation{\tM}{\rho}{\tytv} =

813: \interpretation{\tM}{\rho'}{\tytv}$;

814: \item\label{hl5}

815: $\interpretation{\lambda x.\tM}{\rho}{\tytv} =

816: \interpretation{\lambda y.\tM[y/x]}{\rho}{\tytv}$, if

817: $y\notin\FV(\tM)$;

818: \item\label{hl6}

819: $(\forall X\in\SF. \interpretation{\tM}{\rho[X/x]}{\tytv} =

820: \interpretation{\tN}{\rho[X/x]}{\tytv})\;\Rightarrow\;

821: \interpretation{\lambda x.\tM}{\rho}{\tytv} =

822: \interpretation{\lambda x.\tN}{\rho}{\tytv}$.

823: \end{enumerate}

824: Moreover it is extensional, that is $\interpretation{\lambda

825: x.\tM x}{\rho}{\tytv} = \interpretation{\tM}{\rho}{\tytv}$  when

826: $x\notin\FV(\tM)$.

827: \end{theorem}

828: 

829: 

830: \section{Simple easy terms and filters}\label{section-simple-easy-terms}

831: In this section we give the main notion of the paper, namely

832: {\em simple easiness}. A term $\tE$ is simple easy if,

833: given any eitt $\Sigma^{\tytv}$ and

834: a type $Z\in\type^\tytv$, we can extend in a conservative

835: way $\Sigma^{\tytv}$ to $\Sigma^{\tytv'}$, so that

836: $\interpretation{\tE}{}{\tytv'}=

837: \FFF{\tytv'} Z\sqcup\interpretation{\tE}{}{\tytv}$.

838: This allows to build with an uniform

839: technique filter models in which the

840: interpretation of $\tE$ is {\em a filter of types induced by a predicate}

841: (see Definition \ref{nice}).

842: 

843: 

844: 

845: \begin{definition}\label{filter-scheme}$\;$

846: \begin{enumerate}

847: \item

848: Let be $\sar{\tytv}$ and $\sar{\tytv'}$ two eitts. We say that $\sar{\tytv'}$ is a {\em conservative extension} of $\sar{\tytv}$ (notation

849: $\sar{\tytv}\sqsubseteq\sar{\tytv'}$) iff

850: $\con^\tytv\subset\con^{\tytv'}$ and for all

851: $A,B\in\type^\tytv$,

852: \[A\leq_\tytv B\;\Leftrightarrow\; A\leq_{\tytv'} B.\]

853: \item

854: A {\em pointed\/} eitt is a pair

855: $(\Sigma^{\tytv}, Z)$ with $Z\in\type^{\tytv}$.

856: \item A {\em filter scheme\/} is a mapping

857: $\filterscheme:\mbox{\it PEITT}\rightarrow\mbox{\it EITT}$, such that

858: for any $(\Sigma^\tytv,Z)$

859: \[\Sigma^\tytv\sqsubseteq \filterscheme(\Sigma^\tytv,Z),\;\]

860: where {\it EITT} and

861: {\it PEITT} denote respectively the classes of

862: eitts and pointed eitts.

863: \end{enumerate}

864: \end{definition}

865: 

866: 

867: We now give the central notion of {\em simple easy\/} term.

868: 

869: \begin{definition}\label{simply-easy}$\;$\\

870: An unsolvable term $\tE$ is {\em simple easy\/} if there

871: exists a filter scheme $\filterscheme_\tE$ such that for any pointed

872: eitt $(\Sigma^\tytv, Z)$,

873: \[\vdash^{ \tytv'} \tE:B \iff \exists

874: C\in\type^\tytv. C\cap Z\leq_{\tytv'} B\;\&\;\ctas \tE:C,\]

875: where $\Sigma^{\tytv'} = \filterscheme_\tE(\Sigma^\tytv,Z)$.$\;$

876: \end{definition}

877: 

878: A first key property of easy terms is showed in  \cite{aleslusi02}.

879: 

880: \begin{theorem}\label{E-prende-Z}$\;$\\

881: With the same notation of previous definition, we have

882: $\interpretation{\tE}{}{\tytv'} =

883: \FFF{\tytv'} Z\sqcup \interpretation{\tE}{}{\tytv}$.

884: \end{theorem}

885: 

886: The last notion we need is that of filters induced by a predicate.

887: 

888: 

889: \begin{definition}\label{nice}$\;$\\\

890: Let $\p$ be a predicate defined on $\typetytv$ for all $\tytv$.

891: The $\tytv$-filter induced by $\p$ is the filter defined by:

892: \[X^{\tytv}_\p=\FFF{\tytv}\set{A\in\typetytv\mid \p(A)}.\]

893: \end{definition}

894: %%%%%%%%%%%%%%%%%%%%%%

895: 

896: \begin{theorem}\label{manca}$\;$\\

897: Let $\tE$ be a simple easy term and $\p$ be as in previous definition. Then there is a filter model in which the interpretation of $\tE$ is the filter induced by $\p$.

898: \end{theorem}

899: {\em Proof.}\ \ \ \

900: Let $\langle \cdot,\cdot\rangle$

901: denotes any fixed bijection between $\naturali\times\naturali$ and

902: $\naturali$ such that $\langle r,s\rangle \geq r$.

903: 

904: We will define a denumerable sequence of eitts $\Sigma^{\tytv_{0}}, \ldots,\Sigma^{\tytv_{r}}, \ldots$. For each $r$ we will consider

905: a fixed enumeration $\langle W^{(r)}_{s}\rangle_{s\in\mbox{I$\!$N}}$ of the set 

906: $\set{A\in \type^{\tytv_{r}} \mid A\notin \type^{\tytv_{r-1}}\&\p(A)}$ (for $r=0$ the clause

907: $A\notin \type^{\tytv_{r-1}}$ is vacously true).

908: 

909: We can construct the model as follows.\smallskip

910: 

911: \noindent

912: {\bf step\/} $0$:\ \ \

913: take the eitt $\Sigma^{\tytv_{0}}$

914: whose filter

915: model is isomorphic to Scott $D_{\infty}$ (see \cite{coppdezahonslong84}):\\

916: ${}$\ \ - $\con^{\tytv_{0}} = \{\tyt,\omega\}$;\\

917: ${}$\ \  - $\tytv_{0} =

918:     \overline{\tytv}\cup\{\omega\sim\tyt\rightarrow\omega\}$.\smallskip

919: 

920: \noindent

921: {\bf step\/} $(n+1)$:\ \ \

922: if $n=\langle r,s\rangle$ we define $\Sigma^{\tytv_{n+1}} =

923: \filterscheme_{\tE}(\Sigma^{\tytv_{n}}, W^{(r)}_{s})$ (notice that $\Sigma^{\tytv_{n}}\sqsubseteq\Sigma^{\tytv_{n+1}}$);

924: \smallskip

925: 

926: \noindent

927: {\bf final step}:\ \ \ take $\Sigma^{\tytv_{*}}=\Sigma(\bigcup_{n} \con^{\tytv_{n}},

928: \bigcup_{n} \tytv_{n})$.

929: \smallskip

930: 

931: We prove first that the model ${\cal F}^{\tytv_{*}}$ is non-trivial by

932:  showing that

933: $\interpretation{\sf i}{}{\tytv_{*}}\neq

934: \interpretation{\sf k}{}{\tytv_{*}}$, where ${\sf i}\equiv\lambda x.x$

935: ${\sf k}\equiv\lambda xy.x$. Let $D\equiv(\omega\to\omega)\to(\omega\to\omega)$.

936: Since

937: $\vdash^{\tytv_{*}}{\sf i}:D$,

938: we have that $D\in

939: \interpretation{\sf i}{}{\tytv_{*}}$.

940: On the other hand, if it were

941: $D\in\interpretation{\sf k}{}{\tytv_{*}}$, then it should exists

942: $n$ such that

943: $D\in\interpretation{\sf k}{}{\tytv_{n}}$. This would imply

944: (by applying several times the Generation Theorem)

945: $\omega\to\omega\leq_{\tytv_{n}} \omega$. Since we have

946: $\Sigma^{\tytv_{n}}\sqsubseteq \Sigma^{\tytv_{n+1}}$ for any $n$,

947: we should have $\omega\to\omega\leq_{\tytv_{0}} \omega$.

948: Since $\omega\sim_{\tytv_{0}}\tyt\to\omega$, we should conclude,

949: by Theorem \ref{strong-beta-are-beta},

950: $\tyt\leq_{\tytv_{0}} \omega$, which is a contradiction.

951: Therefore we cannot have $D\in\interpretation{\sf k}{}{\tytv_{*}}$

952: and the model ${\cal F}^{\tytv_{*}}$ is non-trivial.

953: 

954: Now we prove that $\interpretation{\tE}{}{\tytv_{*}}=

955:  \FFF{\tytv_{*}} \set{W^{(r)}_{s} \mid  r,s\in\naturali}$ by showing that 

956: $\interpretation{\tE}{}{\tytv_{n}}=

957:  \FFF{\tytv_{n}} \set{W^{(r)}_{s} \mid \langle r,s\rangle< n}$ for all $n$.

958: The inclusion 

959: $(\supseteq)$ is immediate by construction. We prove $(\subseteq)$ by induction on $n$.

960: If $n=0$, then $\interpretation{\tE}{}{\tytv_{0}}=\FFF{\tytv_{0}}\tyt$,

961: since ${\cal F}^{\tytv_{0}}$ is the Scott $D_{\infty}$ model,

962: where all unsolvable terms are equated to bottom.

963: Suppose the thesis true for $n=\langle r_n,s_n\rangle$

964: and let $B\in\interpretation{\tE}{}{\tytv_{n+1}}$.

965: Then $\vdash^{\tytv_{n+1}} \tE:B$. This is possible only if

966: there exists $C\in \type^{\tytv_{n}}$ such that

967: $C\into W^{(r_n)}_{s_n}\leq_{\tytv_{n+1}} B$ and moreover

968: $\vdash^{\tytv_{n}} \tE:C$. By induction

969: we have $C\in\FFF{\tytv_{n}}\set{W^{(r)}_{s} \mid \langle r,s\rangle< n}$,

970: hence $W^{(r_1)}_{s_1}\into\ldots\into W^{(r_k)}_{s_k}\leq_{\tytv_{n}} C$  for some

971: $r_1,\ldots, r_k, s_1,\ldots, s_k$ with $\langle r_i,s_i\rangle< n$ $(1\leq i\leq k)$.

972: We

973: derive $W^{(r_1)}_{s_1}\into\ldots\into W^{(r_k)}_{s_k}\into W^{(r_n)}_{s_n}\leq_{\tytv_{n+1}} B$, i.e. $B\in  \FFF{\tytv_{n+1}} \set{W^{(r)}_{s} \mid \langle r,s\rangle< n+1}$ .

974: 

975: Finally we show that $A\in\type^{\tytv_{*}}$ and $\p(A)$ iff $A\equiv W^{(r)}_{s}$ for some $r,s$.

976: If $A\in\type^{\tytv_{*}}$ then there is an $r$ such that $A\in\type^{\tytv_{r}}$ and $A\notin\type^{\tytv_{r-1}}$.   Moreover if $\p(A)$ holds there is $s$ such that 

977: $A\equiv W^{(r)}_{s}$. The vice versa is immediate. So we can conclude $\interpretation{\tE}{}{\tytv_{*}} = 

978:  \uparrow \set{A\in \type^{\tytv_{*}} \mid \p(A)}$, i.e. $\interpretation{\tE}{}{\tytv_{*}}=X^{\tytv_*}_\p$.

979: 

980: \section{An application to the consistency of $\lambda$-theories}\label{appl}

981: We introduce now a $\lambda$-theory whose consistency has been first proved

982: using a suitable filter model \cite{lusisali02}. We obtain the same model here as a

983: consequence of Theorem \ref{manca}. Let $\Delta\equiv\lambda x.xx$.

984: 

985: \begin{definition}

986: The $\lambda$-theory $\cJ$ is

987: axiomatized by

988: \[

989: \gO xx = x;\quad \gO xy = \gO yx;\quad \gO x(\gO yz) = \gO (\gO xy)z.

990: \]

991: \end{definition}

992: 

993: It is clear that the previous equations hold if the interpretation of $\gO$ is the join operator on filters.

994: For using Theorem \ref{manca} we need:

995: \begin{itemize}

996: \item $\gO$ to be simple easy;

997: \item the join operator on filters to be a filter generated by a predicate defined on all types.

998: \end{itemize}

999: 

1000: The first condition is proved in \cite{aleslusi02}. For the second one it is easy to check that the join 

1001: relative to $\SF$ is represented by the filter:

1002: \[\FFF{\tytv_{}}\set{A\to B\to A\into B}.\]

1003: Therefore the required predicate is

1004: \[\p(C)= (C\equiv A\to B\to A\into B).\]

1005: 

1006: We can conclude:

1007: 

1008: \begin{theorem}

1009: The $\lambda$-theory $\cJ$ is consistent.

1010: \end{theorem}

1011: 

1012: Previous result is used in \cite{lusisali02} to show that there exists a sublattice of the lattice of $\lambda$-theories

1013: which satisfies a restricted form of distributivity, called meet

1014: semidistributivity,

1015: and a nontrivial congruence identity (i.e., an identity in the language

1016: of lattices enriched by the relative product of binary relations).

1017: 

1018: \section{Conclusion}

1019: 

1020: The notions of simple easy terms and filter models have been successfully applied to show easiness of $\lambda$-terms \cite{aleslusi02}.

1021: The present paper is a first step toward the application of this methodology for proving consistency of $\lambda$-theories. As a side-effect we showed that simple easiness is more general than easiness. The question whether easiness implies simple easiness remains open. An interesting research direction which we plan to follow is the characterization of the $\lambda$-theories whose consistency can be shown using the present approach or some generalizations of it.

1022: 

1023: \begin{thebibliography}{l}

1024: {

1025:  \bibitem {abra91}S. Abramsky. Domain theory in logical form.

1026: {\em Ann. Pure Appl. Logic}. 51(1-2):1-77, 1991. 

1027: 

1028: \bibitem{alesdezahons01}F. Alessi, M.

1029: Dezani-Ciancaglini. Filter models and easy terms. In {\em ICTCS'01}, vol. 2202 of {\em LNCS}, pages 17-37. Springer, Berlin, 2001.

1030: 

1031: \bibitem{aleslusi02} F. Alessi, S. Lusin. Simple easy terms. In {\em ITRS'02}, vol. 70 of {\em ENTCS}. Elsevier, 2002.

1032: 

1033: \bibitem {baetboer79}J.Baeten and B. Boerboom. $\Omega$ can be anything it shouldn't be. {\em

1034: Indag. Math.}, 41:111-120, 1979.

1035: 

1036: \bibitem {barecoppdeza83}H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini.

1037: A filter lambda model and the completeness of type assignment.

1038: {\em  J. Symbolic Logic}, 48(4):931-940, 1983.

1039: 

1040: \bibitem{coppdeza80}M.Coppo and M. Dezani-Ciancaglini.

1041:     An extension of the basic functionality theory for the $\lambda

1042:              $-calculus.

1043:   {\em Notre Dame J. Formal Logic}, 21(4):685-693, 1980.

1044: 

1045: \bibitem{coppdezahonslong84}M.Coppo, M. Dezani-Ciancaglini, F. Honsell,

1046: and G. Longo. Extended type structures and filter lambda models.

1047: In {\em Logic colloquium '82}, pages 241-262.

1048:     North-Holland, Amsterdam, 1984.

1049: 

1050: \bibitem{coppdezavenn80} M. Coppo, M. Dezani-Ciancaglini, and B.

1051: Venneri. Principal type schemes and $\lambda $-calculus semantics.

1052: In {\em To H. B. Curry: essays on combinatory logic, lambda

1053: calculus and formalism}, pages 535-560. Academic Press, London,

1054: 1980.

1055: 

1056: \bibitem{coppdezazacc87} M.Coppo, M. Dezani-Ciancaglini, and M. Zacchi.

1057: Type theories, normal forms, and ${D}\sb \infty$-lambda-models.

1058: {\em Inform. and Comput.}, 72(2):85-116, 1987.

1059: 

1060: \bibitem{dezahonsmoto2000} M. Dezani-Ciancaglini, F. Honsell,  and Y. Motohama.

1061: Compositional characterization of $\lambda$-terms

1062:                   using Intersection Types. In {\em MFCS'00}, vol. 1893 of {\em LNCS}, pages 304-313, Springer, 2000.

1063: 

1064: 

1065: \bibitem{hindlong80}R. Hindley  and G. Longo. Lambda-calculus models and extensionality.

1066:   {\em Z. Math. Logik Grundlag. Math.}, 26(4):289-310, 1980.

1067: 

1068:   \bibitem{kupe97} J. Kuper. On the Jacopini tecnique. {\em Inform. and Comput.}, 138:101-123, 1997.

1069: 

1070: \bibitem{lusisali02} S. Lusin

1071:          and A. Salibra, The lattice of lambda theories, submitted, 2002.

1072: 

1073: 

1074: \bibitem{plot93} G. D. Plotkin. Set-theoretical and other elementary models of the

1075:              $\lambda$-calculus. {\em Theoret. Comput. Sci.},

1076:              121(1-2):351-409, 1993. 

1077: 

1078:  \bibitem {pott80} G. Pottinger. A type assignment for the strongly normalizable $\lambda

1079:              $-terms. In {\em To H. B. Curry: essays on combinatory logic, lambda

1080: calculus

1081:              and formalism}, pages 561-577. Academic Press, London, 1980.

1082: 

1083: 

1084: 

1085: \bibitem{scot72} D. Scott. Continuous lattices. In {\em Toposes, algebraic geometry and logic}, pages 97-136. vol. 274 of {\em LNM}. Springer,

1086: Berlin, 1972.

1087: 

1088: 

1089: 

1090: \bibitem{zylb91} C. Zylberajch. {\em Syntaxe et Semantique de la Facilit\'e en Lambda-calcul}.

1091: PhD thesis, Universit\'e Paris VII, 1991.

1092: }

1093: \end{thebibliography}

1094: \end{document}

1095: