Skip to content

Deciding property for enumerable set #1373

@uzytkownik

Description

@uzytkownik
Contributor

If we can prove ¬ ((n : ℕ) → ¬ P n) for some decidable property P we can get ∃ P

{-# TERMINATING #-}
enumerable :  {p} {P : Pred ℕ p}  Decidable {A = ℕ} P   ¬ ((n : ℕ)  ¬ P n)  ∃ P
enumerable {P = P} dec f with dec zero
... | yes p[zero] = zero , p[zero]
... | no  ¬p[zero] with enumerable {P = P ∘ suc} (dec ∘ suc) λ n→P[1+n]  f λ {zero  ¬p[zero]; (suc n)  n→P[1+n] n}
...  | n , p[n] = suc n , p[n]

The question becomes if this function terminates:

  • According to rules of classical logic it does
  • According to rules of intuitionistic logic it is unprovable that it does terminate from what I understand

This property is much weaker than double negation axiom:

  • It works only for enumerable sets
  • It works only for decidable properties
  • It is however 'safer' than double negation in agda as value is not a ⊥

Activity

MatthewDaggitt

MatthewDaggitt commented on Dec 8, 2020

@MatthewDaggitt
Contributor

What exactly is your question or your proposal? 😄

gallais

gallais commented on Dec 8, 2020

@gallais
Member

Related idea: Coq's constructive epsilon module.

uzytkownik

uzytkownik commented on Dec 9, 2020

@uzytkownik
ContributorAuthor

@MatthewDaggitt

I guess question:

  • Should this be in agda?
  • If yes where it should be?
  • If yes how should it be named?
MatthewDaggitt

MatthewDaggitt commented on Dec 9, 2020

@MatthewDaggitt
Contributor

In theory I have no objections to it. The usual approach is to put the type definition in Axiom.X where X is the name of the axiom that you would like to add to the system. You can then take the axiom in as an assumption to a particular proof in the library and hence remain --safe.

As for the name, I'm sure there's probably an official one somewhere which I'd advocate using. Otherwise I might be tempted to go with something like the super-catchy CountableDecidableExistential? Another question is would we want the type to be over naturals or over any type that is Countable? The latter definition doesn't yet exist in the library...

gallais

gallais commented on Dec 9, 2020

@gallais
Member

It's called Markov's Principle

jamesmckinna

jamesmckinna commented on Feb 6, 2025

@jamesmckinna
Contributor

Is it --safe to add an Axiom (qua definition...) which depends on the {-# TERMINATING ... #-} pragma?

gallais

gallais commented on Feb 7, 2025

@gallais
Member

Axioms are never safe

jamesmckinna

jamesmckinna commented on Feb 7, 2025

@jamesmckinna
Contributor

Axioms are never safe

Well... yes, but the stdlib approach to 'axiom's is (usually) pure Searleian 'if-then-ism'. What makes this one different is the use of (external) appeal to the termination checker to justify a definition. The question was a technical one about whether the use of {-# TERMINATING #-} is compatible with --safe. But my instinct tells me it can't be?

gallais

gallais commented on Feb 7, 2025

@gallais
Member

My reponse was purely technical: it cannot be accepted by --safe.

That being said, I am more than happy to have it in the stdlib (together with its properties).

jamesmckinna

jamesmckinna commented on Feb 7, 2025

@jamesmckinna
Contributor

My reponse was purely technical: it cannot be accepted by --safe.

🎉 thanks!

jamesmckinna

jamesmckinna commented on Feb 7, 2025

@jamesmckinna
Contributor

That being said, I am more than happy to have it in the stdlib (together with its properties).

So, could we imagine an 'if-then-ism' factorisation, with Axiom.MarkovPrinciple stating the property, and its consequence (which would be --safe?), and an unsafe implementation using the {-# TERMINATING #-} proof given above?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

      Development

      No branches or pull requests

        Participants

        @uzytkownik@gallais@MatthewDaggitt@jamesmckinna

        Issue actions

          Deciding property for enumerable set · Issue #1373 · agda/agda-stdlib