Kirill Elagin | 29 Jul 23:26 2014
Picon

Theoretical limits of termination checking (reference request)

Hello,

I was going through the great articles by Andreas Abel and I suddenly started asking myself very basic questions about theoretical limits of termination checking. The halting problem is often cited as an explanation for impossibility of sound&complete termination checker. The termination checking problem is not exactly the halting problem, but indeed it is quite easy to derive impossibility of general termination checking from impossibility of solving the halting problem.

But then, another question arises. When we encode proofs, say, in Agda, we often have a terminating program in mind, but we have to write it down in some specific way, so that the termination checker “sees” that the program is fine. So, is it possible to develop a “programming style” such that there is a sound&complete termination checker for programs “written in this style”, _and_ any program can be “written in this style” (the “translation” function is obviously not computable)? Formally: is there a subset of programs, such that there is an algorithm correctly checking termination of programs from this subset _and_ for any program there is an equivalent in this subset (by “equivalent” I mean “extensionally equal”)?
I used to think that it is impossible, but I recently realized that my “proof” was wrong. Turns out that when we are working with the whole universe of programs, undecidability of termination checking follows from undecidability of the halting problem. But if we restrict ourselves to a subset, it is no longer necessarily true, and sound&complete termination checking (for programs from this subset) _is_ possible for some subsets.

Then, there are more questions. How good can we become at translating arbitrary programs to equivalents from some of those good subsets? As I said, the translation function is clearly not computable. But can it be that it is not computable only for programs we don't care about? Or maybe it is not computable by algorithms, but computable by human brains? Are any of the existing means of checking termination already “perfect” in this sense, that is can I write _any_ terminating function, say, in MiniAgda, so that it passes the termination check?
I haven't come up with any answers to those ones yet.

For some reason I couldn’t find any information on this topic. I guess that either those questions are so trivial and the answers to them are so obvious that no one even bothers to write them down, or everything about this was published long ago in 70s, so it’s somewhat difficult to find those papers now.
I feel that negative results are most likely to come from the computability theory, while positive ones—from more specific fields.

Is there an ultimate source of this kind of funny, useless, purely theoretical facts?
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Andrés Sicard-Ramírez | 31 Jul 05:12 2014
Picon

Agda executables names

Since the Agda maintenance executables names are suffixed by the version
(e.g. agda-2.4.0.3 and agda-mode-2.4.0.3), is there some Emacs
configuration advice for using the different executables names?

Thanks,
--
Andrés
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Andreas Abel | 29 Jul 22:22 2014
Picon
Picon

Agda 2.4.0.2 released

The next maintenance release of Agda 2.4.0 is out!  It has mainly 
bug-fixes, plus a few small new features.

Get it with cabal from hackage or download from the Agda wiki!

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download

   https://hackage.haskell.org/package/Agda

Have fun,
Andreas

Important changes since 2.4.0.1:

* The Agda input mode now supports alphabetical super and subscripts,
   in addition to the numerical ones that were already present.
   [Issue 1240]

* New feature: Interactively split result.

   Make case (C-c C-c) with no variables given tries to split on the
   result to introduce projection patterns.  The hole needs to be of
   record type, of course.

     test : {A B : Set} (a : A) (b : B) → A × B
     test a b = ?

   Result-splitting ? will produce the new clauses:

     proj₁ (test a b) = ?
     proj₂ (test a b) = ?

   If hole is of function type ending in a record type, the necessary
   pattern variables will be introduced before the split.  Thus, the
   same result can be obtained by starting from:

     test : {A B : Set} (a : A) (b : B) → A × B
     test = ?

* The so far undocumented ETA pragma now throws an error if applied to
   definitions that are not records.

   ETA can be used to force eta-equality at recursive record types,
   for which eta is not enabled automatically by Agda.
   Here is such an example:

     mutual
       data Colist (A : Set) : Set where
         [] : Colist A
         _∷_ : A → ∞Colist A → Colist A

       record ∞Colist (A : Set) : Set where
         coinductive
         constructor delay
         field       force : Colist A

     open ∞Colist

     {-# ETA ∞Colist #-}

     test : {A : Set} (x : ∞Colist A) → x ≡ delay (force x)
     test x = refl

   Note:  Unsafe use of ETA can make Agda loop, e.g. by triggering
   infinite eta expansion!

* Bugs fixed (see https://code.google.com/p/agda/issues):
   1203
   1205
   1209
   1213
   1214
   1216
   1225
   1226
   1231
   1233
   1239
   1241
   1243

--

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel@...
http://www2.tcs.ifi.lmu.de/~abel/
Jesper Cockx | 28 Jul 10:46 2014
Picon

AIM XX

Dear all,

On the page of AIM XIX (http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXIX) it still says that there are three possible dates for AIM XX (25-29 Aug, 4-10 Sep or 8-12 Sep). Is there any concrete information which of these dates has been chosen (if any)? I'd very much like to know before the end of this week, because otherwise I won't be able to attend.

Cheers,
Jesper
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Emiliano Tramontana | 26 Jul 10:53 2014
Picon

Call for Papers PSC track at SAC 2015


CALL FOR PAPERS

Programming for Separation of Concerns (PSC) Track at ACM SAC 2015

http://www.dmi.unict.it/~tramonta/sac/

Important Dates
-------------
Paper Due September 12, 2014
Student Research Abstract Due September 12, 2014

Author Notification November 17, 2014
Camera Ready Dicember 8, 2014
Registration Dicember 15, 2014

Conference in Salamanca, Spain April 13-17, 2015

Call for Papers
-----------

Modularity issues tackled by Separation of Concerns (SoC) techniques such as computational reflection,
aspect-oriented programming (AOP), subject-oriented programming (SOP) and context-oriented
programming (COP) have been successfully employed to produce systems whose concerns are well
separated, thereby facilitating reuse and evolution of system components or systems as a whole.

The Programming for Separation of Concerns (PSC) track at the 2015 Symposium on Applied Computing (SAC)
aims to explore challenges that developers currently face when using SoC techniques during development
and evolution.

This year we aim at finding whether solutions based on SoC techniques can be appropriate for dealing with
distributed and parallel systems, such as cloud computing and GPGPUs.  Moreover, we aim at finding out how
to change legacy systems in order to improve their modularity, hence the techniques helping
rejuvenation.  In this sense, we encourage submissions related with strategies that aim at tackling the
discovery of faults related with distribution, parallelisation and ageing.  The track will address
questions like: how such techniques cope with architectural erosion? Are these techniques helpful to
deal with evolution of legacy systems?  Is there a need to extend current technologies supporting SoC?

Authors are invited to submit original papers. Submissions are encouraged, but not limited, to the
following topics:
- Software architectures 
- Configuration management systems
- Software reuse and evolution of legacy systems
- Performance issues for metalevel and aspect-oriented systems (AOSD)
- Testing of aspect-based systems
- Mining of faults on aspect-based systems
- Consistency, integrity and security
- Generative approaches
- Analysis and evaluation of software systems
- Experiences in using reflection, composition filters, aspect- subject- and feature- orientation, and change-oriented-software-engineering
- Reflective and aspect-oriented middleware for distributed systems
- Language support for aspect-oriented and SoC systems
- Modelling of SoC techniques to allow predictable outcomes from their use
- Formal methods for metalevel and SoC systems

Submission Guidelines
------------------

Original papers from the above mentioned or other related areas will be considered. Only full papers about
original and unpublished research are sought.  Parallel submission to other conferences or tracks is not acceptable.

Papers can be submitted in electronic format via the SAC website within 12 September 2014.  http://www.acm.org/conferences/sac/sac2015/Paper-SubmissionUploadPage.htm
Please make sure that the authors name and affiliation do not appear on the submitted paper.

Peer groups with expertise in the track focus area will blindly review submissions to the track.

At least one author of the accepted paper should register and participate in the PSC track.  Accepted papers
will be published in the annual conference ACM proceedings.

The camera-ready version of the accepted paper should be prepared using the ACM format (guidelines will be
given on the SAC website). The maximum number of pages allowed for the final papers is six (6), with the
option, at additional cost, to add two (2) more pages.

A set of papers submitted to the PSC track and not accepted as full papers will be selected as poster papers
and published in the ACM proceedings as 2-page papers, with the option, at additional cost, to add one (1)
more page.

      
Paper registration is required, allowing the inclusion of the paper/poster in the conference
proceedings. An author or a proxy attending SAC MUST present the paper.  This is a requirement for the
paper/poster to be included in the ACM/IEEE digital library.  No-show of scheduled papers and posters
will result in excluding them from the ACM/IEEE digital library.

Student Research Competition
------------------------

Graduate students are invited to submit their work as abstract research paper within within 12 September
2014 (minimum two pages, maximum four pages). The work has to be authored by one student only. The abstract
should reflect on the originality and innovation of the approach, and applicability of preliminary
results to real-world problems. All abstracts must be submitted via SAC website.

Authors of selected abstracts are eligible to apply to the SIGAPP Student Travel Award program for support.

Please contact the track chairs for any further information needed.
Joachim Breitner | 26 Jul 15:08 2014
Picon

Maintenance status of Agda dependencies

Hi,

I’m still working on packaging Agda 2.4 for Debian. It has a few new
dependencies, among them "boxes". But it seems that boxes is not an
actively developed library:

https://github.com/Eelis/boxes/issues/4#issuecomment-50233208

Are the Agda developers are going to care about such dependencies?

In general I’d advise to be selective in what you depend on. Hackage is
a code dump, and not everything there has the stability and maintenance
status that a high-profile package like Agda should demand.

It would also make downstream packager’s work easier.

Greetings,
Joachim

--

-- 
Joachim “nomeata” Breitner
  mail@...http://www.joachim-breitner.de/
  Jabber: nomeata@...  • GPG-Key: 0xF0FBF51F
  Debian Developer: nomeata@...

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Maurizio Proietti | 24 Jul 22:44 2014
Picon

LOPSTR 2014: Call for Participation

===================== CALL FOR PARTICIPATION =============================

                                               24th International Symposium on
                               Logic-Based Program Synthesis and Transformation
                                                             LOPSTR 2014

                                         http://www.iasi.cnr.it/events/lopstr14/
                          University of Kent, Canterbury, UK, September 9-11, 2014

                  Co-located with the 16th International ACM SIGPLAN Symposium on 
                    Principles and Practice of Declarative Programming (PPDP 2014)

==========================================================================
Early registration by August 8, 2014

Invited Speakers:
     Roberto Giacobazzi (University of Verona, Italy)
"Obscuring Code -- Unveiling and Veiling Information in Programs"
     Viktor Kuncak (EPFL, Switzerland)
Title to be announced

Accepted papers
- Nikita Danilenko
Functional Kleene Closures
- Amer Tahat and Ali Ebnenasir
A Hybrid Method for the Verification and Synthesis of Parameterized Self-Stabilizing Protocols
- German Vidal
Concolic Execution and Test-Case Generation in Prolog
- Henning Christiansen and Maja Kirkeby
Confluence Modulo Equivalence in Constraint Handling Rules
- Remis Balaniuk
Drill & Join: A method for inductive program synthesis
- Minoru Kinoshita, Kohei Suenaga and Atsushi Igarashi
Automatic Synthesis of Combiners in the MapReduce Framework - An Approach with Right Inverse
- Daniel De Schreye, Vincent Nys and Colin Nicholson
Analysing and Compiling Coroutines with Abstract Conjunctive Partial Deduction
- Daniel Gall and Thom Frühwirth
A Formal Semantics for the Cognitive Architecture ACT-R
- J. Robert M. Cornish, Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard and Peter J. Stuckey
Analyzing array manipulating programs by program transformation
- Nada Sharaf, Slim Abdennadher and Thom Frühwirth
A Visualization Tool for Constraint Handling Rules
- Salvador Lucas, Jose Meseguer and Raúl Gutiérrez
Extending the 2D DP Framework for CTRSs
- Ahmed Nagah, Amira Zaki and Slim Abdennadher
Exhaustive Execution of CHR through Source-to-Source Transformation
- Sandra Alves, Anatoli Degtyarev and Maribel Fernandez
Access control and obligations in the category-based metamodel: A rewrite-based semantics
- James Lipton, Emilio Jesús Gallego Arias and Julio Mariño
A Declarative Compilation of Constraint Logic Programming
- Jose F. Morales and Manuel V. Hermenegildo
Pre-indexed Terms for Prolog
- Norbert Preining, Kokichi Futatsugi and Kazuhiro Ogata
Liveness properties in CafeOBJ - a case study for meta-level specifications
- Wlodzimierz Drabent
On completeness of logic programs
- Ranjeet Singh and Andy King
Partial Evaluation for Java Malware Detection
- Raul Gutierrez and Salvador Lucas
Below Frozen Positions
- Md Solimul Chowdhury, Jia-Huai You, Wu Chen, Arash Karimi and Fangfang Liu
Polynomial Approximation to Well-Founded Semantics for Logic Programs with Generalized Atoms: Case Studies
=============================================================================

Program Co-Chairs:
     Maurizio Proietti, IASI-CNR, Italy (maurizio.proietti-faJWBVtKsas1GQ1Ptb7lUw@public.gmane.org)
     Hirohisa Seki, Nagoya Institute of Technology, Japan (seki-755XKL+rTlTtP0S62TOXqw@public.gmane.org)

Symposium Co-Chairs:
     Olaf Chitil and Andy King
     School of Computing, University of Kent, UK 

Organizing Committee:
     Emanuele De Angelis, University of Chieti-Pescara and IASI-CNR, Italy 
     Fabrizio Smith, IASI-CNR, Italy
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Hongseok Yang | 24 Jul 18:49 2014
Picon

HOPE 2014 Call for Participation (with Workshop Program)

----------------------------------------------------------------------

                      CALL FOR PARTICIPATION

                           HOPE 2014

                The 3rd ACM SIGPLAN Workshop on
              Higher-Order Programming with Effects

                        August 31, 2014
                      Gothenburg, Sweden
                   (the day before ICFP 2014)


----------------------------------------------------------------------

HOPE 2014 aims at bringing together researchers interested in the design, 
semantics, implementation, and verification of higher-order effectful 
programs. It will be *informal*, consisting of invited talks, contributed 
talks on work in progress, and open-ended discussion sessions. 


------------
Registration
------------

Deadline for early registration: 3 August 2014

This is the registration site for ICFP 2014 and all the affiliated
workshops including HOPE 2014.


------------
Invited Talk
------------

Title: Verifying Security Properties of SES Programs
Speaker: Philippa Gardner, Imperial College London


----------------------
List of Accepted Talks
----------------------

(1) Stevan Andjelkovic. Towards indexed algebraic effects and handlers

(2) Kwok Cheung. Separating Entangled State

(3) Filip Sieczkowski and Lars Birkedal. ModuRes: a Coq Library for Reasoning about Concurrent Higher-Order Imperative Programming Languages

(4) Ohad Kammar. Graphical algebraic foundations for monad stacks

(5) Paul Downen and Zena M. Ariola. Delimited control with multiple prompts in theory and practice

(6) Carter Schonwald. A Type Directed model of Memory Locality and the design of High Performance Array APIs

(7) Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Derek Dreyer and Viktor Vafeiadis. Compositional Compiler Verification via Parametric Simulation

(8) Danel Ahman and Tarmo Uustalu. From stateful to stackful computation


---------------------
Goals of the Workshop
---------------------

A recurring theme in many papers at ICFP, and in the research of many
ICFP attendees, is the interaction of higher-order programming with
various kinds of effects: storage effects, I/O, control effects,
concurrency, etc. While effects are of critical importance in many
applications, they also make it hard to build, maintain, and reason
about one's code. Higher-order languages (both functional and
object-oriented) provide a variety of abstraction mechanisms to help
"tame" or "encapsulate" effects (e.g. monads, ADTs, ownership types,
typestate, first-class events, transactions, Hoare Type Theory,
session types, substructural and region-based type systems), and a
number of different semantic models and verification technologies have
been developed in order to codify and exploit the benefits of this
encapsulation (e.g. bisimulations, step-indexed Kripke logical
relations, higher-order separation logic, game semantics, various
modal logics). But there remain many open problems, and the field is
highly active.

The goal of the HOPE workshop is to bring researchers from a variety
of different backgrounds and perspectives together to exchange new and
exciting ideas concerning the design, semantics, implementation, and
verification of higher-order effectful programs.

We want HOPE to be as informal and interactive as possible. The
program will thus involve a combination of invited talks, contributed
talks about work in progress, and open-ended discussion
sessions. There will be no published proceedings, but participants
will be invited to submit working documents, talk slides, etc. to be
posted on this website.


---------------------
Workshop Organization
---------------------

Program Co-Chairs:

Neel Krishnaswami (University of Birmingham)
Hongseok Yang (University of Oxford)


Program Committee:

Zena Ariola (University of Oregon)
Ohad Kammar (University of Cambridge)
Ioannis Kassios (ETH Zurich)
Naoki Kobayashi (University of Tokyo)
Paul Blain Levy (University of Birmingham)
Aleks Nanevski (IMDEA)
Scott Owens (University of Kent)
Sam Staton (Radboud University Nijmegen)
Steve Zdancewic (University of Pennsylvania)
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Nicolas Wu | 23 Jul 11:44 2014
Picon
Picon

ICFP Programming Contest 2014

=====================================================================
                      Call for Participation

                The 17th ICFP Programming Contest

                    http://www.icfpcontest.org
                 Friday 25 July 2014 at 12:00 UTC
=====================================================================

The ICFP Programming Contest 2014 is starting at the end of this week!

It's nearly time to roll up your sleeves, and gain fame and glory for your
programming language of choice: prepare for sleepless nights and hours of fun!

The full details of the contest specification will appear on the contest
website at http://www.icfpcontest.org on Friday 25 July 2014 at 12:00 UTC.
No registration is required: just roll up and have some fun!

For more announcements, stay tuned on our twitter feed at:

https://twitter.com/icfpcontest2014

Good luck to all participants,

Nicolas Wu
Dan Krejsa | 21 Jul 23:53 2014
Picon

Re: Re: Data.Vec toList - fromList isomorphism

Hi,

The _=v=_ version of equality that I introduced, and the awkward 'transfer' use, turn
out not to be needed if one maps between List A and Σ ℕ (λ n -> Vec A n):

listToVec : ∀ {i} {A : Set i} -> List A -> Σ ℕ (λ n -> Vec A n)
listToVec [] = ℕ.zero , []
listToVec (x ∷ l) = let (n , v) = listToVec l in ℕ.suc n , x ∷ v

vecToList : ∀ {i} {A : Set i} -> Σ ℕ (λ n -> Vec A n) -> List A
vecToList (.ℕ.zero , []) = []
vecToList (.(ℕ.suc _) , x ∷ v) = x ∷ vecToList (_ , v)

L-V-L : ∀ {i} {A : Set i} -> (l : List A) -> vecToList (listToVec l) ≡ l
L-V-L [] = refl
L-V-L (x ∷ l) = cong (_∷_ x) (L-V-L l)

V-L-V : ∀ {i} {A : Set i} -> (v : Σ ℕ (λ n -> Vec A n)) -> listToVec (vecToList v) ≡ v
V-L-V (.ℕ.zero , []) = refl
V-L-V (ℕ.suc n  , x ∷ v) with listToVec (vecToList (n , v)) | V-L-V (n , v)
V-L-V (ℕ.suc n , x ∷ v) | .n , .v | refl = refl

Figuring out how to get the equality working on the Σ type was a bit tricky for me.

- Dan



On Sun, Jul 20, 2014 at 12:44 PM, Dan Krejsa <dan.krejsa-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org> wrote:
Thanks, Ulf!

In my actual application I'm using (Fin n -> A) to represent the vectors (since I want
to look at permutations / bijections of Fin n), but I may take a similar approach to
what you do above.

Also, I'll take a look at agda-prelude.
The main awkwardness I think is the need to resort to 'transport' at all, but
maybe that's unavoidable if I'm trying to get a propositional equality (at
least pointwise for Fin n -> A) rather than being content with something like VecEq.

- Dan

P.S. It may also help to extend the toList / fromList mappings to non-dependent
mappings between (List A) and Σ ℕ (λ n -> Vec A n), and maybe hide the
nasty 'transport' inside an appropriate equality operator on Σ ℕ (λ n -> Vec A n),
maybe something like this:

listToVec : ∀ {i} {A : Set i} -> List A -> Σ ℕ (λ n -> Vec A n)
listToVec [] = ℕ.zero , []
listToVec (x ∷ l) =
    let (n , v) = listToVec l
    in ℕ.suc n , x ∷ v

vecToList : ∀ {i} {A : Set i} -> Σ ℕ (λ n -> Vec A n) -> List A
vecToList (.0 , []) = []
vecToList (.(ℕ.suc _) , x ∷ v) = x ∷ vecToList (_ , v)

L-V-L : ∀ {i} {A : Set i} -> (l : List A) -> vecToList (listToVec l) ≡ l
L-V-L [] = refl
L-V-L (x ∷ l) = cong (_∷_ x) (L-V-L l)

infix 2 _=v=_

_=v=_ : ∀ {i} {A : Set i} -> (v w : Σ ℕ (λ n -> Vec A n)) -> Set i
_=v=_ {A = A} (n , v) (m , w) = Σ (n ≡ m) (λ n≡m -> transport (Vec A) n≡m v ≡ w)

_∷'_ : ∀ {i} {A : Set i} -> A ->  Σ ℕ (λ n -> Vec A n) ->  Σ ℕ (λ n -> Vec A n)
x ∷' (n , v) = ℕ.suc n , x ∷ v

=v=cons : ∀ {i} {A : Set i} {v w : Σ ℕ (λ n -> Vec A n)} (a : A) -> v =v= w -> a ∷' v =v= a ∷' w
=v=cons {v = n , v} {.n , w} a (refl , tv=w) = refl , cong (_∷_ a) tv=w

V-L-V : ∀ {i} {A : Set i} -> (v : Σ ℕ (λ n -> Vec A n)) -> listToVec (vecToList v) =v= v
V-L-V (.0 , []) = refl , refl
V-L-V (ℕ.suc n  , x ∷ v) = =v=cons x (V-L-V (n , v))





On Sun, Jul 20, 2014 at 1:19 AM, Ulf Norell <ulf.norell <at> gmail.com> wrote:
Not sure if you find this less awkward, but here is a different, slightly less ad-hoc, approach (using my prelude library [1] rather than the standard library).

open import Prelude

-- Heterogenous equality on vectors --

VecEq : ∀ {a} {A : Set a} {n m} (xs : Vec A n) (ys : Vec A m) → Set a
VecEq []       []       = ⊤′
VecEq []       (x ∷ ys) = ⊥′
VecEq (x ∷ xs) []       = ⊥′
VecEq (x ∷ xs) (y ∷ ys) = x ≡ y × VecEq xs ys

-- If vectors are equal then the lengths are equal
vecEq-len : ∀ {a} {A : Set a} {n m} (xs : Vec A n) (ys : Vec A m) →
              VecEq xs ys → n ≡ m
vecEq-len [] [] heq = refl
vecEq-len [] (x ∷ ys) ()
vecEq-len (x ∷ xs) [] ()
vecEq-len (_ ∷ xs) (_ ∷ ys) (_ , heq) =
  cong suc (vecEq-len xs ys heq)

-- VecEq xs ys implies transport xs ≡ ys
vecEq-≡ : ∀ {a} {A : Set a} {n m} (xs : Vec A n) (ys : Vec A m) (n=m : n ≡ m) →
            VecEq xs ys → transport (Vec A) n=m xs ≡ ys
vecEq-≡ [] [] refl heq = refl
vecEq-≡ (x ∷ xs) (.x ∷ ys) refl (refl , heq) =
  cong (_∷_ x) (vecEq-≡ xs ys refl heq)

-- Vec to List round-trip --

-- This proof is super-easy
v-l-v′ : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
           VecEq (listToVec (vecToList xs)) xs
v-l-v′ []       = _
v-l-v′ (x ∷ xs) = refl , v-l-v′ xs

-- We can get the original theorem from the VecEq lemmas
lentoList : ∀ {a} {A : Set a} {n} (xs : Vec A n) → length (vecToList xs) ≡ n
lentoList xs = vecEq-len (listToVec (vecToList xs)) xs (v-l-v′ xs)

v-l-v : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
        transport (Vec A) (lentoList xs) (listToVec (vecToList xs)) ≡ xs
v-l-v xs = vecEq-≡ (listToVec (vecToList xs)) xs (lentoList xs) (v-l-v′ xs)

/ Ulf



On Sun, Jul 20, 2014 at 3:22 AM, Dan Krejsa <dan.krejsa-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org> wrote:
Hi,

I figured out a proof for v-l-v using a lemma transLenSuc,

-----
transLenSuc :  ∀ {i} {A : Set i} {n m : ℕ} -> (p : n ≡ m) -> (a : A) -> (v : Vec A n)
     -> transLen (cong ℕ.suc p) (a ∷ v) ≡ a ∷ transLen p v
transLenSuc refl a v = refl


v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) ->  transLen (lentoList v) (fromList (toList v)) ≡ v
v-l-v [] = refl
v-l-v (x ∷ v) = trans (transLenSuc (lentoList v) x (fromList (toList v))) (cong (_∷_ x) (v-l-v v))
-----

but the approach still seems kind of awkard, so suggestions still appreciated.

- Dan



On Sat, Jul 19, 2014 at 4:37 PM, Dan Krejsa <dan.krejsa-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org> wrote:
Hi,

It's pretty clear that the toList and fromList functions in Data.Vec are in some
sense inverses.  One direction is easy to show:

l-v-l : ∀ {i} {A : Set i} (l : List A) -> toList (fromList l) ≡ l
l-v-l [] = refl
l-v-l (x ∷ l) = cong (λ xs → x ∷ xs) (l-v-l l)

In the other direction my first naive attempt

v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -> fromList (toList v) ≡ v
v-l-v v = ?

fails with Agda complaining about (fromList (toList v) ≡ v) since equality is
homogeneous and

   fromList (toList v)

has type

  Vec A (length (toList v))

which is not judgementally equal to the type of v, which is (Vec A n),
although that equality is easy to show propositionally:

lentoList : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -> length (toList v) ≡ n
lentoList [] = refl
lentoList (x ∷ v) = cong ℕ.suc (lentoList v)

My next attempt was to try to use the equality (lentoList v) as a 'cast' to convert the type of fromList (toList v)

transport : ∀ {i j} {A : Set i} (B : A -> Set j) {x y : A} -> x ≡ y -> B x -> B y
transport B refl = id

transLen : ∀ {i} {A : Set i} {n m : ℕ} -> n ≡ m -> Vec A n -> Vec A m
transLen {A = A} n≡m v = transport (λ l -> Vec A l) n≡m v

v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) ->  transLen (lentoList v) (fromList (toList v)) ≡ v
v-l-v [] = refl
v-l-v (x ∷ v) with lentoList v
... | eq = {! !}

but I didn't get much further since Agda does not want to case on 'eq' as a pattern
variable turning it into refl.

My guess is there's probably a standard way around this sort of problem, or
a better way to express that (fromList ∘ toList) is pointwise the same as the identity.
But I'm presently both new & rusty enough not to think of it, having done just a bit of
Agda proving in the past and having been away from it for a while...

Any hints?

- Dan


_______________________________________________
Agda mailing list
Agda-TrQ0NnR75ays1BDpvl8NfQ@public.gmane.orgmers.se
https://lists.chalmers.se/mailman/listinfo/agda




_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Dan Krejsa | 20 Jul 01:37 2014
Picon

Data.Vec toList - fromList isomorphism

Hi,

It's pretty clear that the toList and fromList functions in Data.Vec are in some
sense inverses.  One direction is easy to show:

l-v-l : ∀ {i} {A : Set i} (l : List A) -> toList (fromList l) ≡ l
l-v-l [] = refl
l-v-l (x ∷ l) = cong (λ xs → x ∷ xs) (l-v-l l)

In the other direction my first naive attempt

v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -> fromList (toList v) ≡ v
v-l-v v = ?

fails with Agda complaining about (fromList (toList v) ≡ v) since equality is
homogeneous and

   fromList (toList v)

has type

  Vec A (length (toList v))

which is not judgementally equal to the type of v, which is (Vec A n),
although that equality is easy to show propositionally:

lentoList : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -> length (toList v) ≡ n
lentoList [] = refl
lentoList (x ∷ v) = cong ℕ.suc (lentoList v)

My next attempt was to try to use the equality (lentoList v) as a 'cast' to convert the type of fromList (toList v)

transport : ∀ {i j} {A : Set i} (B : A -> Set j) {x y : A} -> x ≡ y -> B x -> B y
transport B refl = id

transLen : ∀ {i} {A : Set i} {n m : ℕ} -> n ≡ m -> Vec A n -> Vec A m
transLen {A = A} n≡m v = transport (λ l -> Vec A l) n≡m v

v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) ->  transLen (lentoList v) (fromList (toList v)) ≡ v
v-l-v [] = refl
v-l-v (x ∷ v) with lentoList v
... | eq = {! !}

but I didn't get much further since Agda does not want to case on 'eq' as a pattern
variable turning it into refl.

My guess is there's probably a standard way around this sort of problem, or
a better way to express that (fromList ∘ toList) is pointwise the same as the identity.
But I'm presently both new & rusty enough not to think of it, having done just a bit of
Agda proving in the past and having been away from it for a while...

Any hints?

- Dan
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda

Gmane