From 1f7da57279ce037054198cb09402dcc5f1ac913e Mon Sep 17 00:00:00 2001 From: Matthijs Kooijman Date: Wed, 9 Dec 2009 10:21:09 +0100 Subject: [PATCH] Add a section on proving determinism. --- Chapters/Normalization.tex | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index 8230547..5252c0f 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -2559,5 +2559,25 @@ we need to check every (set of) transformation(s) separately. \todo{Perhaps do a few steps of the proofs as proof-of-concept} + \subsection{Determinism} + A well-known technique for proving determinism in lambda calculus + and other reduction systems, is using the Church-Rosser property + \cite[church36]. A reduction system has the CR property if and only if: + + \placedefinition[here]{Church-Rosser theorem} + {\lam{\forall A, B, C \exists D (A ->> B ∧ A ->> C => B ->> D ∧ C ->> D)}} + + Here, \lam{A ->> B} means \lam{A} \emph{reduces to} \lam{B}. In + other words, there is a set of transformations that can be applied + to transform \lam{A} to \lam{B}. \lam{=>} is used to mean + \emph{implies}. + + For a transformation system holding the Church-Rosser property, it + is easy to show that it is in fact deterministic. Showing that this + property actually holds is a harder problem, but has been + done for some reduction systems in the lambda calculus + \cite[klop80]\ \cite[barendregt84]. Doing the same for our + transformation system is probably more complicated, but not + impossible. % vim: set sw=2 sts=2 expandtab: -- 2.30.2