Тьюринг-полнота

[proger]

Xaositect в сообщении #874678 писал(а):

mu f - минимальное значение, при котором f равна Z, либо бесконечное число x = S(#x).

Я не знаю агду, и долго пытался понять, что у Вас написано, но не понял. Скажите проще. Вы можете на агде написать такой код, который потом запустите, и он будет выполняться бесконечно? Такая программа скомпилируется или нет? Только без фокусов, я знаю, что там можно отключить termination checker как-то. Не отключая его можно или нет?

[Xaositect]

Я сейчас не могу скомпилировать программу на агде, и у меня нет особого желатия выяснять, почему apt install agda не дает мне нужных для этого библиотек.

Суть в том, что тотальные с использованием бесконечных (коиндукивных) структур данных могут быть невычислимыми, т.е. при любой семантике выполнения будут иногда выполняться бесконечно долго.

А так, учитывая, что тамошнее IO построено на коиндуктивных Stream Char, вот, можете попробовать скомпилировать. Termination check проходит.

module Test where

open import Coinduction
open import Data.Unit
open import Data.String
open import Data.Colist
open import IO
open import IO.Primitive as Prim

bangs : Costring
bangs = '!' ∷ (♯ bangs)

main : Prim.IO ⊤
main = run (putStr∞ bangs)

[arseniiv]

proger в сообщении #874859 писал(а):

способ чего?

Способ маркировки побочных эффектов в типах. В каком-то языке пошли дальше и сделали информацию о побочных эффектах более подробной.