[TYPES] Typed lambda calculi with weak conversion

[Thorsten Altenkirch]

Hi Filippo,

you can define weak equality using a substitution calculus. The basic idea is that you have normal forms of the form (\x.t)[us and laws like ((\x.t)[us])[vs] = (\x.t)[us o vs], see http://www.cs.nott.ac.uk/~psztxa/publ/jtait07.pdf, p.6.

Cheers,
Thorsten




On 25/02/2018, 11:06, "Types-list on behalf of Filippo Sestini" <types-list-bounces at LISTS.SEAS.UPENN.EDU on behalf of sestini.filippo at gmail.com> wrote:

>[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>Dear all,
>
>The notion of weak reduction first appeared in [1], and was later
>developed into the definition of a weak lambda calculus in, for
>example, [2]. The crucial property of weak reduction is that it
>does not validate the ξ rule, but some form of computation under
>binders is still possible.
>
>I'm looking for references in the literature treating typed
>calculi with full lambda syntax and weak conversion, in
>particular regarding normalization. What I've found so far seems
>to either be limited to a form of combinator syntax, or only
>consider evaluation to weak head normal form ([3], [4]).
>Do you have any suggestions?
>
>Thank you
>
>Sincerely
>
>[1] W.A. Howard, Assignment of Ordinals to Terms for Primitive
>Recursive Functionals of Finite Type, 1970
>1970
>
>[2] N. Çağman, J.R. Hindley, Combinatory weak reduction in lambda
>calculus, 1998
>
>[3] P. Martin-Löf, An Intuitionistic Theory of Types: Predicative
>Part, 1975
>
>[4] T. Coquand, P. Dybjer, Intuitionistic Model Constructions and
>Normalization Proofs, 1998
>
>-- 
>Filippo Sestini
>sestini.filippo at gmail.com
>(+39) 333 6757668
>