Relating the λσ- and λs-styles of explicit substitutions

Fairouz Kamareddine, Alejandro Rìos

Research output: Contribution to journalArticle

16 Citations (Scopus)

Abstract

Two methods of explicit substitutions, ?s- and ?s-styles, are compared. A criterion of adequacy is used to simulate ß-reduction in calculi of explicit substitutions and apply it to several calculi: ?s; ?s?; ?v; ?s; ?t; and ?u. Results proved that ?t is more adequate than ?v and that ?u is more adequate that ?v, ?s?, and ?s. Counterexamples is given to show that all other comparisons are impossible according to the criterion.

Original languageEnglish
Pages (from-to)349-380
Number of pages32
JournalJournal of Logic and Computation
Volume10
Issue number3
Publication statusPublished - Jun 2000

Fingerprint Dive into the research topics of 'Relating the λσ- and λs-styles of explicit substitutions'. Together they form a unique fingerprint.

Cite this