Showing 1–2 of 2 results for author: Cherevichenko, G

Alpha-conversion for lambda terms with explicit weakenings

Authors: George Cherevichenko

Abstract: Using explicit weakenings, we can define alpha-conversion by simple equations without any mention of free variables. Using explicit weakenings, we can define alpha-conversion by simple equations without any mention of free variables. △ Less

Submitted 24 December, 2018; originally announced December 2018.

Is alpha-conversion easy?

Authors: George Cherevichenko

Abstract: We present a new lambda-calculus with explicit substitutions and named variables. Renaming of bound variables in this calculus is explicit (there is a special rewrite rule) and can be delayed. Contexts (environments) are not sets or lists without multiplicity, but have a more complicated structure. There is a natural order on the set of contexts. A "set" of free variables is not a set, but a conte… ▽ More We present a new lambda-calculus with explicit substitutions and named variables. Renaming of bound variables in this calculus is explicit (there is a special rewrite rule) and can be delayed. Contexts (environments) are not sets or lists without multiplicity, but have a more complicated structure. There is a natural order on the set of contexts. A "set" of free variables is not a set, but a context in the new sense. New definitions simplify working with alpha-conversion. △ Less

Submitted 1 April, 2014; v1 submitted 20 March, 2013; originally announced March 2013.

Comments: Bibliography was expanded, nothing else