[Agda] Does the order of patterns matter?
Andreas Abel
andreas.abel at ifi.lmu.de
Sat Sep 29 00:28:26 CEST 2012
Hi Thorsten,
On 28.09.12 2:35 PM, Altenkirch Thorsten wrote:
> Hi Andreas,
>
> did you produce the parallel substitution function by splitting or by hand?
Sorry, that is a while ago, I do not remember.
> It seems to me that the issue only arises with hand crafted patterns but
> not patterns that are produced by splitting. Is this correct?
Well, no, if you start with
subst : ∀ {m} {vt : VarTrm m} (tau : RenSub vt) → Tm → Tm
subst tau t = {!!}
then split on t
subst tau (var x) = {!!}
subst tau (abs t) = {!!}
subst tau (app t t₁) = {!!}
then modify the first clause to
subst {vt = vt} tau (var x) = {!!}
and split on vt, you get the final clauses
subst {.0} {Var} tau (var x) = ?
subst {.1} {Trm} tau (var x) = ?
subst tau (abs t) = {!!}
subst tau (app t t₁) = {!!}
where the last two equations will not hold definitionally.
The order in which the user did the splitting is not recorded, so when
Agda loads the above clauses, it internally reconstructs a different
split order. This is because it makes no effort avoid unnecessary
splits. It just picks the first non-variable pattern (here,
paradoxically, Var), and splits on that argument.
I enclose the Agda file for your own experimentation...
Cheers,
Andreas
> On 28/09/2012 12:15, "Andreas Abel" <andreas.abel at ifi.lmu.de> wrote:
>
>> Martin,
>>
>> I agree that equations not holding definitionally is a major source of
>> confusion. I back your proposal, but to realize it in full would be a
>> bigger change of the theory of definitional equality. It would take us
>>from a theory based on eliminators or computational rules to a theory
>> with more general rewriting rules.
>>
>> But at least, there should be a way of telling Agda that one want the
>> equations to hold, and that it should be an error if Agda cannot make it
>> work (needs more splitting than one specified). Here is an issue for
>> this on the bug tracker:
>>
>> http://code.google.com/p/agda/issues/detail?id=408
>>
>> Cheers,
>> Andreas
>>
>> On 27.09.12 12:51 PM, Martin Escardo wrote:
>>> Nils' message tells us where to find a full explanation of what is going
>>> on.
>>>
>>> On 27/09/12 11:27, Altenkirch Thorsten wrote:
>>>> The bug is rather that we use the = sign here -
>>>> Epigram avoided this by using |-> and it also kept track of the
>>>> splittings.
>>>
>>> But "|->" would also be wrong, because e.g. in Achim's example, there is
>>> a situation f lhs = rhs where there is no reduction f lhs |-> rhs. But
>>> this is just a notational discussion
>>>
>>>
>>> Here are some questions/conjectures.
>>>
>>> (1) It would be possible to implement Agda so that each equation in a
>>> pattern holds definitionally, if we wished, I believe. Of course, you
>>> would get new definitional equalities not present in Martin-Loef type
>>> theory. But does that matter? Conjecture: no new propositional
>>> equalities arise.
>>>
>>> (2) Every equation in a definition by pattern matching should hold
>>> propositionally (we know that this is not the case definitionally).
>>> This should be a meta-theorem.
>>>
>>> (3) Is there a nice characterization of pattern-matching definitions
>>> such that every "definining equation" does hold definitionally? The
>>> Berry-function in Nils' response indicates that this may be hard. Such
>>> pattern-system should be invariant under permuting equations, in
>>> suitable sense.
>>>
>>> (4) What is there against forcing defining equations to hold
>>> definitionally, other than being able to compile them to
>>> eliminator-trees? Already in definitions by pattern matching on natural
>>> numbers there is a departure from Martin-Lof type theory, because in
>>> MLTT you need an inductive definition to even compute the predecessor
>>> function. So why not go a bit further, provide (1) and (2) make sense?
>>>
>>> It is very disturbing that a proof ceases to type check if we reorder
>>> mutually exclusive, complete patterns.
>>>
>>> Such an extension should be conservative in the sense of allowing more
>>> proofs, but no new theorems. (Which the eta-rule doesn't satisfy, but
>>> nevertheless we seem to be happy to add.)
>>>
>>> Best,
>>> Martin
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
>> --
>> Andreas Abel <>< Du bist der geliebte Mensch.
>>
>> Theoretical Computer Science, University of Munich
>> Oettingenstr. 67, D-80538 Munich, GERMANY
>>
>> andreas.abel at ifi.lmu.de
>> http://www2.tcs.ifi.lmu.de/~abel/
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
> This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.
>
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses which could damage your computer system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
-------------- next part --------------
-- Parallel substitution as an operation for untyped de Bruijn terms
-- Author: Andreas Abel
-- Date : 2011-03-01
--
-- Instead of distinguishing renamings and substitutions as in
--
-- Chung-Kil Hur et al.,
-- Strongly Typed Term Representations in Coq
--
-- which leads to 4 different composition operations,
-- we define a generic substitution/renaming operation.
-- This is inspired by
--
-- Conor McBride
-- Type Preserving Renaming and Substitution
--
-- but, being not restricted to structural recursion, we can utilize
-- the lexicographically terminating definition of
--
-- Thorsten Altenkirch and Bernhard Reus
-- Monadic Presentations of Lambda Terms Using Generalized Inductive Types
--
-- This way, we have a single composition operation and lemma, which is mutual
-- with a lemma for composition of liftings.
module ParallelSubstitution where
open import Data.Nat
open import Relation.Binary.PropositionalEquality renaming (subst to coerce)
open ≡-Reasoning
-- since we model substitutions as functions over natural numbers
-- (instead of lists), functional extensionality is very convenient to have!
postulate
funExt : ∀ {A : Set}{B : Set}{f g : A → B} →
(∀ x → f x ≡ g x) → f ≡ g
-- De Bruijn lambda terms
data Tm : Set where
var : (x : ℕ) → Tm
abs : (t : Tm) → Tm
app : (t u : Tm) → Tm
-- A structurally ordered two-element set
data VarTrm : ℕ → Set where
Var : VarTrm 0 -- we are dealing with variables (natural numbers)
Trm : VarTrm 1 -- we are dealing with terms
max01 : ℕ → ℕ → ℕ
max01 0 m = m
max01 n m = n
compVT : ∀ {n m} (vt : VarTrm n) (vt' : VarTrm m) → VarTrm (max01 n m)
compVT Var vt' = vt'
compVT Trm vt = Trm
-- A set of variables or terms
VT : ∀ {n} → (vt : VarTrm n) → Set
VT Var = ℕ
VT Trm = Tm
-- A mapping which is either a renaming (Var) or substitution (Trm)
RenSub : ∀ {n} → (vt : VarTrm n) → Set
RenSub vt = ℕ → VT vt
Ren = ℕ → ℕ -- Renamings
Subst = ℕ → Tm -- Substitutions
-- We define lifting in terms of substitution
-- See, e.g., Altenkirch and Reus, CSL 1999
mutual
lift : ∀ {m} {vt : VarTrm m} (tau : RenSub vt) → RenSub vt
-- lifting a renaming
lift {vt = Var} tau 0 = 0
lift {vt = Var} tau (suc x') = suc (tau x')
-- lifting a substituion
lift {vt = Trm} tau 0 = var 0
lift {vt = Trm} tau (suc x') = subst suc (tau x') -- shift
-- FAILS: result from interactive splitting
subst : ∀ {m} {vt : VarTrm m} (tau : RenSub vt) → Tm → Tm
subst {.0} {Var} tau (var x) = var (tau x)
subst {.1} {Trm} tau (var x) = tau x
subst tau (abs t) = abs (subst (lift tau) t)
subst tau (app t t₁) = app (subst tau t) (subst tau t₁)
{- -- WORKS: manually reordered clauses
subst : ∀ {m} {vt : VarTrm m} (tau : RenSub vt) → Tm → Tm
subst {vt = vt } tau (abs t) = abs (subst (lift tau) t)
subst {vt = vt } tau (app t u) = app (subst tau t)
(subst tau u)
-- PUT THESE LAST BECAUSE OF AGDA SPLIT HEURISTICS:
subst {vt = Var} tau (var x) = var (tau x) -- lookup in renaming
subst {vt = Trm} tau (var x) = tau x -- lookup in substitution
-}
-- substitution composition
comp : ∀ {n}{vt2 : VarTrm n}(tau : RenSub vt2)
{m}{vt1 : VarTrm m}(sigma : RenSub vt1) → RenSub (compVT vt1 vt2)
comp tau {vt1 = Var} sigma x = tau (sigma x)
comp tau {vt1 = Trm} sigma x = subst tau (sigma x)
-- Composition lemma
mutual
comp_lift :
∀ {n}{vt2 : VarTrm n}(tau : RenSub vt2)
{m}{vt1 : VarTrm m}(sigma : RenSub vt1) →
comp (lift tau) (lift sigma) ≡ lift (comp tau sigma)
comp_lift tau sigma = funExt (comp_lift' tau sigma)
comp_lift' :
∀ {n}{vt2 : VarTrm n}(tau : RenSub vt2)
{m}{vt1 : VarTrm m}(sigma : RenSub vt1)(x : ℕ) →
comp (lift tau) (lift sigma) x ≡ lift (comp tau sigma) x
comp_lift' {vt2 = Var} tau {vt1 = Var} sigma zero = refl
comp_lift' {vt2 = Trm} tau {vt1 = Var} sigma zero = refl
comp_lift' {vt2 = Var} tau {vt1 = Trm} sigma zero = refl
comp_lift' {vt2 = Trm} tau {vt1 = Trm} sigma zero = refl
comp_lift' {vt2 = Var} tau {vt1 = Var} sigma (suc x') = refl
comp_lift' {vt2 = Trm} tau {vt1 = Var} sigma (suc x') = refl
comp_lift' {vt2 = Var} tau {vt1 = Trm} sigma (suc x') = begin
subst (lift tau) (subst suc (sigma x'))
≡⟨ comp_subst (lift tau) suc (sigma x') ⟩
subst (comp (lift tau) suc) (sigma x')
≡⟨ refl ⟩
subst (λ x → comp (lift tau) suc x) (sigma x')
≡⟨ refl ⟩
subst (λ x → suc (tau x)) (sigma x')
≡⟨ refl ⟩
subst (λ x → comp suc tau x) (sigma x')
≡⟨ refl ⟩
subst (comp suc tau) (sigma x')
≡⟨ sym (comp_subst suc tau (sigma x')) ⟩
subst suc (subst tau (sigma x'))
∎
comp_lift' {vt2 = Trm} tau {vt1 = Trm} sigma (suc x') = begin
subst (lift tau) (subst suc (sigma x'))
≡⟨ comp_subst (lift tau) suc (sigma x') ⟩
subst (comp (lift tau) suc) (sigma x')
≡⟨ refl ⟩
subst (λ x → comp (lift tau) suc x) (sigma x')
≡⟨ refl ⟩
subst (λ x → subst suc (tau x)) (sigma x') -- distinct line!
≡⟨ refl ⟩
subst (λ x → comp suc tau x) (sigma x')
≡⟨ refl ⟩
subst (comp suc tau) (sigma x')
≡⟨ sym (comp_subst suc tau (sigma x')) ⟩
subst suc (subst tau (sigma x'))
∎
comp_subst :
∀ {n}{vt2 : VarTrm n}(tau : RenSub vt2)
{m}{vt1 : VarTrm m}(sigma : RenSub vt1)(t : Tm) →
subst tau (subst sigma t) ≡ subst (comp tau sigma) t
comp_subst {vt2 = Var} tau {vt1 = Var} sigma (var x) = refl
comp_subst {vt2 = Var} tau {vt1 = Trm} sigma (var x) = refl
comp_subst {vt2 = Trm} tau {vt1 = Var} sigma (var x) = refl
comp_subst {vt2 = Trm} tau {vt1 = Trm} sigma (var x) = refl
comp_subst {vt2 = vt2} tau {vt1 = vt1} sigma (abs t) = begin
subst tau (subst sigma (abs t))
≡⟨ refl ⟩
subst tau (abs (subst (lift sigma) t))
≡⟨ refl ⟩
abs (subst (lift tau) (subst (lift sigma) t))
≡⟨ cong abs (comp_subst (lift tau) (lift sigma) t) ⟩
abs (subst (comp (lift tau) (lift sigma)) t)
≡⟨ cong (λ sigma' → abs (subst sigma' t)) (comp_lift tau sigma) ⟩
abs (subst (lift (comp tau sigma)) t)
≡⟨ refl ⟩
subst (comp tau sigma) (abs t)
∎
comp_subst {vt2 = vt2} tau {vt1 = vt1} sigma (app t u) = begin
subst tau (subst sigma (app t u))
≡⟨ refl ⟩
app (subst tau (subst sigma t)) (subst tau (subst sigma u))
≡⟨ cong (λ t' → app t' (subst tau (subst sigma u)))
(comp_subst tau sigma t) ⟩
app (subst (comp tau sigma) t) (subst tau (subst sigma u))
≡⟨ cong (λ u' → app (subst (comp tau sigma) t) u')
(comp_subst tau sigma u) ⟩
app (subst (comp tau sigma) t) (subst (comp tau sigma) u)
≡⟨ refl ⟩
subst (comp tau sigma) (app t u)
∎
More information about the Agda
mailing list