2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




На страницу Пред.  1, 2
 
 Re: Тьюринг-полнота
Сообщение13.06.2014, 18:29 
Xaositect в сообщении #874678 писал(а):
mu f - минимальное значение, при котором f равна Z, либо бесконечное число x = S(#x).

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

 
 
 
 Re: Тьюринг-полнота
Сообщение13.06.2014, 20:17 
Аватара пользователя
Я сейчас не могу скомпилировать программу на агде, и у меня нет особого желатия выяснять, почему 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)

 
 
 
 Re: Тьюринг-полнота
Сообщение13.06.2014, 20:33 
proger в сообщении #874859 писал(а):
способ чего?
Способ маркировки побочных эффектов в типах. В каком-то языке пошли дальше и сделали информацию о побочных эффектах более подробной.

 
 
 [ Сообщений: 18 ]  На страницу Пред.  1, 2


Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group