Czy można udowodnić, że funkcja jest idempotentna?

Czy można użyć typów statycznych lub zależnych, aby udowodnić, że funkcja jest idempotentna?

Przeszukałem Google i różne miejsca na StackOverflow / StackExchange w celu znalezienia odpowiedzi bez powodzenia. Najbliżej znalazłem rozmowę o Idrisie: https://groups.google.com/forum/#!topic/idris-lang/yp7vrspChRg

Niestety ta dyskusja jest trochę ponad moją głową.

haskell

— bmaddy
źródło

Nie zamieszczam tego jako odpowiedzi, ponieważ nie jestem w 100% pewien, ale uważam, że jest to niemożliwe z powodu twierdzenia Rice'a .

— ogrodnik

To fascynujące pytanie, a moja intuicja wskazuje, że powinno to być możliwe w ograniczonym, niekompletnym języku Turinga. Programiści koncentrują się jednak na pytaniach dotyczących cyklu życia oprogramowania (szczegóły w centrum pomocy ), podczas gdy wydaje się, że jest to pytanie z zakresu informatyki. Witryna informatyki może być lepiej dopasowana i prowadzić do lepszych odpowiedzi.

— amon

Twierdzenie @gardenhead Rice stwierdza, że biorąc pod uwagę jakąkolwiek właściwość, jaką może mieć zachowanie programu, czasami niemożliwe jest ustalenie, czy program ma tę właściwość. Istnieje duża różnica między „czasem jest to niemożliwe” a „to jest niemożliwe”.

— Tanner Swett,

Mój ostatni komentarz był dość niejasny. W każdym razie oto, co mówi twierdzenie Rice'a: nie ma algorytmu, który poprawnie klasyfikowałby wszystkie funkcje jako idempotentne lub idempotentne. Jednak nadal istnieją przydatne algorytmy, które klasyfikują niektóre funkcje jako idempotentne lub nie.

— Tanner Swett

OP poprosił o udowodnienie, że funkcja jest idempotentna, ponieważ nie ma algorytmu klasyfikującego funkcje jako idemptotentne. Główną różnicą jest to, że osoba może napisać dowód. Jeśli chodzi o kompletność Turinga, to naprawdę nie stanowi problemu .

— gallais

Tak jest w przypadku niektórych funkcji. Zwłaszcza gdy znasz funkcję ;-)

Jeśli masz na myśli swoje pytanie „czy istnieje algorytm, który automatycznie decyduje, czy dowolna funkcja jest idempotentna, czy nie”, odpowiedź brzmi „nie” z powodu twierdzeń już wspomnianych w komentarzach. Jednak w przypadku określonych klas funkcji można - teoretycznie - bardzo łatwo zdecydować, czy funkcja jest idempotentna, czy nie. Na przykład, jeśli funkcja jest czysta (oznacza: bez żadnych skutków ubocznych) i wiadomo, że zawsze zwraca wartość w skończonym czasie dla dowolnego podanego wejścia, wtedy o idempotencji można zdecydować po prostu wypróbowując, czy f(f(x))=f(x)dla jakiegokolwiek możliwego wejścia xdo funkcji. Nie żeby to było bardzo wydajne, mogłoby działać do końca wszechświata.

Więc jeśli nie jest to odpowiedź, której szukasz, napisz lepsze pytanie, obecnie nie jest jasne, czego tak naprawdę szukasz.

— Doktor Brown
źródło

Dziękuję za odpowiedź. Możliwość „automatycznego decydowania” była dokładnie tym, czego szukałem.

— bmaddy

Aby rozwinąć wyrażenie „dla niektórych funkcji” : Idempotencja można udowodnić dla dowolnej funkcji, która albo akceptuje tylko skończoną liczbę danych wejściowych (wypróbowując je wszystkie), albo typ danych wejściowych, który jest definiowany rekurencyjnie (jak naturalny liczby lub listy połączone), co oznacza, że wystarczy udowodnić, że idempotencja jest prawdziwa dla przypadków bazowych i przypadków rekurencyjnych.

— Qqwy