{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/3190","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/3190/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/3190/comments","events_url":"https://api.github.com/repos/agda/agda/issues/3190/events","html_url":"https://github.com/agda/agda/issues/3190","id":352620718,"node_id":"MDU6SXNzdWUzNTI2MjA3MTg=","number":3190,"title":"proposal with built-in function for termination ","user":{"login":"mechvel","id":1506057,"node_id":"MDQ6VXNlcjE1MDYwNTc=","avatar_url":"https://avatars3.githubusercontent.com/u/1506057?v=4","gravatar_id":"","url":"https://api.github.com/users/mechvel","html_url":"https://github.com/mechvel","followers_url":"https://api.github.com/users/mechvel/followers","following_url":"https://api.github.com/users/mechvel/following{/other_user}","gists_url":"https://api.github.com/users/mechvel/gists{/gist_id}","starred_url":"https://api.github.com/users/mechvel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mechvel/subscriptions","organizations_url":"https://api.github.com/users/mechvel/orgs","repos_url":"https://api.github.com/users/mechvel/repos","events_url":"https://api.github.com/users/mechvel/events{/privacy}","received_events_url":"https://api.github.com/users/mechvel/received_events","type":"User","site_admin":false},"labels":[{"id":245647354,"node_id":"MDU6TGFiZWwyNDU2NDczNTQ=","url":"https://api.github.com/repos/agda/agda/labels/termination","name":"termination","color":"ededed","default":false},{"id":294947891,"node_id":"MDU6TGFiZWwyOTQ5NDc4OTE=","url":"https://api.github.com/repos/agda/agda/labels/type:%20discussion","name":"type: discussion","color":"d4c5f9","default":false},{"id":245647346,"node_id":"MDU6TGFiZWwyNDU2NDczNDY=","url":"https://api.github.com/repos/agda/agda/labels/type:%20enhancement","name":"type: enhancement","color":"84b6eb","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":12,"created_at":"2018-08-21T16:34:10Z","updated_at":"2018-09-04T09:45:44Z","closed_at":null,"author_association":"NONE","body":"I propose to add to Agda _language_ the construct of well-founded recursion.\r\nI believe it is easy to implement.\r\nThe extension will preserve all the existing applied code.\r\nThe reason for adding this construct is that using the feature of\r\nWellFounded of Standard library complicates programs essentially.\r\nThe extension will preserve all the existing applied code.\r\n  \r\nExample\r\n-----------\r\n\r\n```\r\n--------------------------------------------------------------------\r\ndata Bin : Set      -- A new definition of Bin\r\n     where\r\n     0#    : Bin\r\n     2suc  : Bin → Bin    -- \\n→ 2*(1+n)  arbitrary nonzero even\r\n     suc2* : Bin → Bin    -- \\n→ 1 + 2n   arbitrary odd\r\n\r\n{-# TERMINATING #-}\r\nlog₂ :  (x : Bin) → x ≢ 0# → ℕ      -- integer part of (logarithm₂ x)\r\n\r\nlog₂ 0#                0≢0 =  contradiction refl 0≢0\r\nlog₂ (2suc x)          _   =  1+ (log₂ (suc x) suc≢0)      -- (*)\r\nlog₂ (suc2* 0#)        _   =  0\r\nlog₂ (suc2* (2suc x))  _   =  1+ (log₂ (2suc x)  2suc≢0)\r\nlog₂ (suc2* (suc2* x)) _   =  1+ (log₂ (suc2* x) suc2*≢0)\r\n---------------------------------------------------------\r\n```\r\n`TERMINATING' is set because the rule of (*) is not by a structural  recursion.\r\nThen I prove various properties:\r\n```\r\n---------------------------------------------------------\r\nlog₂∘2* :  (x : Bin) → (nz : x ≢ 0#) → (2x≢0 : 2* x ≢ 0#) → log₂ (2* x) 2x≢0  ≡  1+ (log₂ x nz)\r\nlog₂∘2* 0#        nz  _      =  contradiction refl nz\r\nlog₂∘2* (2suc _)  _    _     =  refl\r\nlog₂∘2* (suc2* x) x'≢0 2x'≢0 =  ...\r\n...\r\n---------------------------------------------------------\r\n```\r\n\r\nTo remove `TERMINATING', it is needed either to add some counter processing to the loop or to apply WellFounded recursion on Bin that uses the inequality  suc x < 2suc x.\r\nThe first approach complicates the program greatly. It becomes considerably more complex than the fragment in possible textbook or a paper:\r\n```\r\n  < The source of log₂ >  \r\n  ++\r\n  \"(*) terminates, because  IsWellFoundedOrder _<_  and because \r\n       lt : suc x < 2suc x\r\n       lt = BinOrd.suc-x<2suc-x x\r\n  \".\r\n ```\r\n\r\nThe second approach currently is possible only by using the feature of WellFounded of Standard library:\r\n```\r\n----------------------------------------------------------------\r\nopen All <-wellFounded using () renaming (wfRec to <-rec)\r\nP :  Bin → Set\r\nP x =  (x ≢ 0#) → ℕ\r\n\r\nlog₂ :  (a : Bin) → P a    -- signature changed \r\nlog₂ =  <-rec _ P log\r\n  where\r\n  log :  (a : Bin) → (∀ x → x < a → P x) → P a\r\n\r\n  log 0#       _      0≢0 =  contradiction refl 0≢0\r\n  log (2suc x) logRec _   =    1+ (logRec (suc x) suc-x<x' suc≢0)\r\n                  where\r\n                  suc-x<x' =  begin suc x       <[ x<2x (suc x) suc≢0  ]\r\n                                              2* (suc x)  ≡[ sym (2suc-as∘ x) ]\r\n                                              2suc x\r\n                                    ∎\r\n\r\n  log (suc2* 0#)        _      _ =  0\r\n  log (suc2* (2suc x))  logRec _ =   1+ (logRec x' (x<suc2*-x x') 2suc≢0)\r\n                                                        where\r\n                                                         x' = 2suc x\r\n\r\n  log (suc2* (suc2* x)) logRec _ =    1+ (logRec x' (x<suc2*-x x') suc2*≢0)\r\n                                                         where\r\n                                                         x' = suc2* x\r\n----------------------------------------------------------------\r\n```\r\n\r\nA proof for  suc-x<x'  is all right, it is needed in any approach.\r\nBut the program is complicated greatly: the signature of \r\n ```\r\n                         (a : Bin) → a ≢ 0# → ℕ\r\n```\r\nis changed to \r\n```\r\n                         (a : Bin) → P a,\r\n```\r\nthe call  ``(<-rec _ P log)``  appears, with a certain complicated signature for  ``log``.\r\n\r\nFurthermore, the proofs are broken. For example, the rule\r\n```\r\n  log₂∘2* (2suc _) _ _ =  refl\r\n```\r\nis not type-checked any more. I expect difficulties in reorganizing proofs.\r\nAnother point:  is this reliable that using   \r\n``<-rec + WellFounded``  does not lead to a run-time cost overhead?\r\n\r\n\r\nProposal\r\n========\r\n\r\nTo add to Agda _language_ the construct of well-founded recursion --\r\nin the following way.\r\n\r\n1. Add to Standard library the notion of  IsWellFoundedOrder : \r\n```\r\n--------------------------------------------------------------------\r\nSequence :  ∀ {α} → (A : Set α) → Set α   -- infinite sequences in A\r\nSequence A =  ℕ → A\r\n\r\nmodule OfWellFounded {α α= α<} (PO : StrictPartialOrder α α= α<)\r\n  where\r\n  open StrictPartialOrder PO using (_≈_; _<_) renaming (Carrier to C)\r\n  _≤_ :  Rel C _\r\n  x ≤ y =  x < y ⊎ x ≈ y\r\n\r\n  DecrementBreak :  Sequence C → Set _\r\n  DecrementBreak f =  ∃ (\\n → f n ≤ f (suc n))\r\n\r\n  IsWellFoundedOrder :  Set _\r\n  IsWellFoundedOrder =  (f : Sequence C) → DecrementBreak f\r\n--------------------------------------------------------------------\r\n```\r\n\r\nThe property is \"any sequence has a decrement break\".\r\n\r\n2. The language construct is as in the following example with  log₂:\r\n```\r\n---------------------------------------------------------------\r\nlog₂ :  (x : Bin) → x ≢ 0# → ℕ    -- signatures do not change!\r\nlog₂ 0#       0≢0 =  contradiction refl 0≢0\r\nlog₂ (2suc x) _   =  1+ (recurseWith isWellFoundedOrder lt  (log₂ (suc x) suc≢0)\r\n                                   )\r\n                              where\r\n                              lt : suc x < 2suc x\r\n                              lt = Ord0.suc-x<2suc-x x\r\n\r\nlog₂ (suc2* 0#)        _ =  0\r\nlog₂ (suc2* (2suc x))  _ =  1+ (log₂ (2suc x)  2suc≢0)\r\nlog₂ (suc2* (suc2* x)) _ =  1+ (log₂ (suc2* x) suc2*≢0)\r\n---------------------------------------------------------------\r\n```\r\nHere the result of \r\n```\r\n         (recurseWith isWellFoundedOrder lt (log₂ (suc x) suc≢0))\r\n```\r\nis   ``(log₂ (suc x) suc≢0)``.\r\n\r\n``recurseWith``  is a built-in function. \r\nIn this example, it makes the type checker to do the following.\r\nIt checks the proofs for  ``lt`` and ``isWellFoundedOrder``,\r\nand thus it concludes that this recursive call of log₂ is well founded.\r\nAs other rules for  ``log₂``  use structural recursion, it concludes that ``log₂``  is terminating.\r\n\r\nThis is a termination _axiom_ by ``IsWellFoundedOrder`` applied by the \r\n_type checker_.\r\n\r\nHow difficult is it to implement in the type checker?\r\nThe user program remains clear.\r\nI hope, the proofs written for the `TERMINATING' version will remain.\r\n\r\nIt is easy to prove  ``IsWellFoundedOrder``  for ``Nat._<_, Bin._<_,`` \r\nand so on.\r\n\r\nI appreciate:  ``WellFounded`` of Standard  is a clever way to bring a traditional termination proof tool without extending language. \r\n\r\nBut it is also desirable to give the possibility to write \"normal\" programs, in the style of somewhat an ordinary mathematical paper, that can be understood by mathematicians (and by the program author himself).\r\nAdvanced algorithms in mathematics need effort to program. \r\nMany people will like rather to use this small language extension than to complicate further the program by artificially changing signatures in a clever way.\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/418307124","html_url":"https://github.com/agda/agda/issues/3190#issuecomment-418307124","issue_url":"https://api.github.com/repos/agda/agda/issues/3190","id":418307124,"node_id":"MDEyOklzc3VlQ29tbWVudDQxODMwNzEyNA==","user":{"login":"gallais","id":1094905,"node_id":"MDQ6VXNlcjEwOTQ5MDU=","avatar_url":"https://avatars1.githubusercontent.com/u/1094905?v=4","gravatar_id":"","url":"https://api.github.com/users/gallais","html_url":"https://github.com/gallais","followers_url":"https://api.github.com/users/gallais/followers","following_url":"https://api.github.com/users/gallais/following{/other_user}","gists_url":"https://api.github.com/users/gallais/gists{/gist_id}","starred_url":"https://api.github.com/users/gallais/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gallais/subscriptions","organizations_url":"https://api.github.com/users/gallais/orgs","repos_url":"https://api.github.com/users/gallais/repos","events_url":"https://api.github.com/users/gallais/events{/privacy}","received_events_url":"https://api.github.com/users/gallais/received_events","type":"User","site_admin":false},"created_at":"2018-09-04T09:45:44Z","updated_at":"2018-09-04T09:45:44Z","author_association":"MEMBER","body":"For what it's worth, I think `Acc` is too low-level to use directly. This is what I\r\nwould do instead (à la Bove-Capretta):\r\n\r\n(`Irrelevant` is in the current dev stdlib, if you use an earlier one you may need\r\nto call it `IrrelevantPred` or something).\r\n\r\n```agda\r\nmodule log where\r\n\r\nopen import Data.Nat renaming (suc to 1+)\r\nopen import Relation.Unary\r\n\r\ndata Bin : Set where\r\n  0#    : Bin\r\n  2suc  : Bin → Bin      -- \\n→ 2*(1+n)  arbitrary nonzero even\r\n  suc2* : Bin → Bin      -- \\n→ 1 + 2n   arbitrary odd\r\n\r\nsuc : Bin → Bin\r\nsuc 0#        = suc2* 0#\r\nsuc (2suc x)  = suc2* (suc x)\r\nsuc (suc2* x) = 2suc x\r\n\r\ndata Log : Bin → Set where\r\n  `2s   : ∀ {x} → Log (suc x) → Log (2suc x)\r\n  `1    : Log (suc2* 0#)\r\n  `s22s : ∀ {x} → Log (2suc x) → Log (suc2* (2suc x))\r\n  `s2s2 : ∀ {x} → Log (suc2* x) → Log (suc2* (suc2* x))\r\n\r\nopen import Relation.Binary.PropositionalEquality\r\n\r\nLog-irrelevance : Irrelevant Log\r\nLog-irrelevance (`2s a)   (`2s b)   = cong `2s (Log-irrelevance a b)\r\nLog-irrelevance `1        `1        = refl\r\nLog-irrelevance (`s22s a) (`s22s b) = cong `s22s (Log-irrelevance a b)\r\nLog-irrelevance (`s2s2 a) (`s2s2 b) = cong `s2s2 (Log-irrelevance a b)\r\n\r\nlog₂ : ∀ {b} → Log b → ℕ\r\nlog₂ (`2s x)   = 1+ (log₂ x)\r\nlog₂ `1        = 0\r\nlog₂ (`s22s x) = 1+ (log₂ x)\r\nlog₂ (`s2s2 x) = 1+ (log₂ x)\r\n\r\n`suc2* : ∀ {b} → Log b → Log (suc2* b)\r\n`suc2* (`2s p)   = `s22s (`2s p)\r\n`suc2* `1        = `s2s2 `1\r\n`suc2* (`s22s p) = `s2s2 (`suc2* p)\r\n`suc2* (`s2s2 p) = `s2s2 (`suc2* p)\r\n\r\n`suc : ∀ {b} → Log b → Log (suc b)\r\n`suc (`2s p)   = `suc2* p\r\n`suc `1        = `2s `1\r\n`suc (`s22s p) = `2s (`suc p)\r\n`suc (`s2s2 p) = `2s (`suc p)\r\n\r\n`2suc  : ∀ {b} → Log b → Log (2suc b)\r\n`2suc (`2s p)   = `2s (`suc2* p)\r\n`2suc `1        = `2s (`2s `1)\r\n`2suc (`s22s p) = `2s (`2suc p)\r\n`2suc (`s2s2 p) = `2s (`2suc p)\r\n\r\ngoal : ∀ {b} (p : Log b) → log₂ (`2suc p) ≡  1+ (log₂ (`suc p))\r\ngoal (`2s p)   = refl\r\ngoal `1        = refl\r\ngoal (`s22s p) = cong 1+ (goal p)\r\ngoal (`s2s2 p) = cong 1+ (goal p)\r\n```"}}
{"actor":{"display_login":"gallais"}}