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.20.1