Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion axioms.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -17170,7 +17170,7 @@ evaluated. See :DOC certify-book, in particular, the discussion about ``Step
; Without the setting of custom:*default-file-encoding* for clisp in
; acl2.lisp, the build breaks with the following string (note the accented "i"
; in Martin, below):
; Francisco J. Mart�n Mateos
; Francisco J. Martín Mateos
; With that setting, we do not need an explicit :external-format argument for
; the call of with-open-file in acl2-check.lisp that opens a stream for
; "acl2-characters".
Expand Down
4 changes: 2 additions & 2 deletions books/defexec/dag-unification/dag-unification-l.lisp
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
;;; ============================================================================
;;; dag-unification-l.lisp
;;; T�tulo: A dag based unification algorithm
;;; Título: A dag based unification algorithm
;;; ============================================================================

#| To certify this book:
Expand All @@ -22,7 +22,7 @@

;;; ============================================================================
;;;
;;; 0) Introducci�n
;;; 0) Introducción
;;;
;;; ============================================================================

Expand Down
4 changes: 2 additions & 2 deletions books/defexec/dag-unification/dag-unification-rules.lisp
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
;;; ============================================================================
;;; dag-unification-rules.lisp
;;; T�tulo: Unification rules on term dags
;;; Título: Unification rules on term dags
;;; ============================================================================

#| To certify this book:
Expand All @@ -21,7 +21,7 @@

;;; ============================================================================
;;;
;;; 0) Introducci�n
;;; 0) Introducción
;;;
;;; ============================================================================

Expand Down
8 changes: 4 additions & 4 deletions books/defexec/dag-unification/dag-unification-st.lisp
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
;;; ============================================================================
;;; dag-unification-st.lisp
;;; T�tulo: A dag based unification algorithm using stobjs
;;; Título: A dag based unification algorithm using stobjs
;;; ============================================================================

#| To certify this book:
Expand All @@ -21,7 +21,7 @@

;;; ============================================================================
;;;
;;; 0) Introducci�n
;;; 0) Introducción
;;;
;;; ============================================================================

Expand Down Expand Up @@ -571,7 +571,7 @@

;;; Guard verification:

;;; REPETIDOS LOS DEJO?
;;; REPETIDOS ¿ LOS DEJO?


(local
Expand Down Expand Up @@ -1176,7 +1176,7 @@

;;; Guard verification

;;; AVERIGUAR POR QU� ESTE TEOREMA TARDA TANTO!!!!!!!!
;;; AVERIGUAR POR QUé ESTE TEOREMA TARDA TANTO!!!!!!!!


;;; I don't know why, but the following theory has an important
Expand Down
10 changes: 5 additions & 5 deletions books/defexec/dag-unification/dags.lisp
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
;;; ============================================================================
;;; dags.lisp
;;; T�tulo: Term dags in ACL2
;;; Título: Term dags in ACL2
;;; ============================================================================

#| To certify this book:
Expand All @@ -18,7 +18,7 @@

;;; ============================================================================
;;;
;;; 0) Introducci�n
;;; 0) Introducción
;;;
;;; ============================================================================

Expand Down Expand Up @@ -510,7 +510,7 @@
(not (dag-p-aux hs rp g)))))

;;; Finally, the soundness theorem:
;;; �������������������������������
;;; ...............................

(defthm dag-p-soundness
(implies (not (dag-p g))
Expand Down Expand Up @@ -554,7 +554,7 @@


;;; The main lemma for completeness:
;;; ��������������������������������
;;; ................................

(local
(defthm dag-p-aux-completeness-main-lemma
Expand Down Expand Up @@ -1601,7 +1601,7 @@


;;; RECALL: These two theorems would allow us to define functions like these:
;;; �������������������������������������������������������������������������
;;; .........................................................................


; (defun occur-check-l (flg x h g)
Expand Down
4 changes: 2 additions & 2 deletions books/defexec/dag-unification/list-unification-rules.lisp
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
;;; ============================================================================;;; list-unification-rules.lisp
;;; T�tulo: Unification as transformation rules
;;; Título: Unification as transformation rules
;;; (using a prefix representation of terms)
;;; ============================================================================

Expand All @@ -17,7 +17,7 @@

;;; ============================================================================
;;;
;;; 0) Introducci�n
;;; 0) Introducción
;;;
;;; ============================================================================

Expand Down
32 changes: 16 additions & 16 deletions books/defexec/dag-unification/matching.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -89,9 +89,9 @@
;;; ----------------------------------------------------------------------------


;;; ����������������������������������������������������������������������������
;;; ............................................................................
;;; 1.2.1 How we deal with selection.
;;; ����������������������������������������������������������������������������
;;; ............................................................................


;;; Firs we prove that equal-set is a congruence w.r.t. the second
Expand Down Expand Up @@ -139,9 +139,9 @@



;;; ����������������������������������������������������������������������������
;;; ............................................................................
;;; 1.2.2 transform-subs-sel preserves the set of matchers.
;;; ����������������������������������������������������������������������������
;;; ............................................................................


(local
Expand Down Expand Up @@ -211,7 +211,7 @@
(not (matcher sigma S)))))

;;; The three main theorems of this subsubsection
;;; ���������������������������������������������
;;; .............................................

(defthm transform-subs-sel-preserves-matchers-1
(implies
Expand All @@ -235,10 +235,10 @@



;;; ����������������������������������������������������������������������������
;;; ............................................................................
;;; 1.2.3 (system-substitution (cdr S-match)) is an invariant in the rules
;;; of transformation.
;;; ����������������������������������������������������������������������������
;;; ............................................................................



Expand All @@ -261,9 +261,9 @@
(system-substitution (cdr (transform-subs-sel S-match)))))))


;;; ����������������������������������������������������������������������������
;;; ............................................................................
;;; 1.2.4 Main property of the property system-substitution
;;; ����������������������������������������������������������������������������
;;; ............................................................................


(local
Expand Down Expand Up @@ -362,7 +362,7 @@
(length-term nil args2))))))

;;; And the main result:
;;; ��������������������
;;; ....................

(defthm transform-subs-sel-decreases-length-of-first-system
(implies (not (normal-form-syst S-match))
Expand Down Expand Up @@ -460,7 +460,7 @@

;;; Three lemmas to state that the set of matchers is preserved by
;;; subs-system-sel
;;; ��������������������������������������������������������������������������
;;; ..........................................................................

(local
(defthm subs-system-sel-preserves-matchers-1
Expand Down Expand Up @@ -488,15 +488,15 @@
(in-theory (enable union-systems))

;;; subs-system-sel preserves the property of being a system-substitution.
;;; ������������������������������������������������������������������
;;; ..................................................................

(local
(defthm subs-system-sel-preserves-system-substitution
(implies (system-substitution (cdr S-match))
(system-substitution (cdr (subs-system-sel S-match))))))

;;; Guard verification: a substitution-s-p is returned
;;; ���������������������������������������������������
;;; ...................................................

(local
(defthm
Expand Down Expand Up @@ -604,7 +604,7 @@
;;; ----------------------------------------------------------------------------

;;; Soundness
;;; ���������
;;; .........


(defthm subs-sel-soundness
Expand All @@ -618,7 +618,7 @@


;;; Completeness
;;; ������������
;;; ............


(defthm subs-sel-completeness
Expand All @@ -632,7 +632,7 @@

;;; Closure property:
;;; (the following theorem is needed for guard verification)
;;; ��������������������������������������������������������
;;; ........................................................


(defthm matching-sel-substitution-s-p
Expand Down
34 changes: 17 additions & 17 deletions books/defexec/dag-unification/subsumption-subst.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -26,15 +26,15 @@
;;; Our goal is to define the subsumption relation between
;;; substitutions. In the literature, this relation is defined in this
;;; way:
;;; sigma <= delta iff (exists gamma) gammasigma = delta
;;; where "" stands for composition.
;;; sigma <= delta iff (exists gamma) gamma.sigma = delta
;;; where "." stands for composition.

;;; Note that equality between substitutions is functional equality (we cannot
;;; use equal), so we reformulate this property as:

;;; (*) sigma <= delta iff (exists gamma)
;;; s.t. for all term
;;; gammasigma(term) = delta(term)
;;; gamma.sigma(term) = delta(term)


;;; Our goal in this book is to define the subsumption relation between
Expand Down Expand Up @@ -285,9 +285,9 @@
;;; if (subs-sust sigma delta)
;;; WE DISTINGUISH THREE CASES.

;;; ����������������������������������������������������������������������������
;;; ............................................................................
;;; 3.1.1 Case 1: x is a variable outside V
;;; ����������������������������������������������������������������������������
;;; ............................................................................



Expand All @@ -303,14 +303,14 @@
:hints (("Goal" :in-theory (enable x-not-in-domain-remains-the-same)))))


;;; ����������������������������������������������������������������������������
;;; ............................................................................
;;; 3.1.2. Case 2: x is a variable of (domain-var sigma)
;;; ����������������������������������������������������������������������������
;;; ............................................................................


;;; 3.1.2.1 A lemma for this case 2:
;;; subs-subst composed with sigma is equal to delta in V.
;;; ������������������������������������������������������
;;; ......................................................

(local
(encapsulate
Expand Down Expand Up @@ -373,7 +373,7 @@
(local (in-theory (disable subs-subst matching-subst)))

;;; 3.1.2.2 Another lemma for case 2:
;;; �������������������������������
;;; ...............................

(local
(defthm variables-co-domain-var
Expand All @@ -383,7 +383,7 @@


;;; 3.1.2.3 The main result for Case 2
;;; ��������������������������������
;;; ................................

(local
(defthm
Expand All @@ -396,14 +396,14 @@
(val x delta)))))


;;; ����������������������������������������������������������������������������
;;; ............................................................................
;;; 3.1.3. Case 3: x in V but not in (domain-var sigma)
;;; ����������������������������������������������������������������������������
;;; ............................................................................


;;; 3.1.3.1 A lemma for Case 3
;;; In this case, matching and matching-subst-r take the same values.
;;; �����������������������������������������������������������������
;;; .................................................................

(local
(defthm
Expand Down Expand Up @@ -472,7 +472,7 @@


;;; With terms and list of terms (not only with variables)
;;; ������������������������������������������������������
;;; ......................................................

(local
(defthm
Expand Down Expand Up @@ -512,7 +512,7 @@
;;; following version will be used as a rewrite rule.

;;; With terms but without using composition
;;; ����������������������������������������
;;; ........................................

(defthm
subs-subst-implies-matching-subst-r-appplied-to-sigma-term-is-delta-term
Expand All @@ -526,7 +526,7 @@


;;; With respect to subsumption between terms
;;; �����������������������������������������
;;; .........................................


;;; Trivial consequence of completeness of subsumption and the previous
Expand Down Expand Up @@ -563,7 +563,7 @@
;;; existence of two substitutions, called sigma-w and delta-w and the
;;; only property we will assume about them is that sigma-w <=
;;; delta-w. That is, exists another substitution gamma-w such that
;;; delta-w = gamma-wsigma-w.
;;; delta-w = gamma-w.sigma-w.

;;; We will use encapsulate for that purpose. Let sigma-w, delta-w and
;;; gamma-w three susbtitutions such that delta-w is functionally equal
Expand Down
Loading