運算の楽しみ - Qiita
プログラム運算 関数プログラミングでは，プログラムは関数として定義します． （この関数は，もちろん計算可能な関数でなければならないという制限はあるものの，数学の対象として扱える関数です．） 単純明瞭な関数定義は，正しいことが明白ではあり，プログラムの仕様として機能します． （すなわち，関数プログラミングにおいてプログラムは実行可能な仕様ということになります．） しかし，単純明瞭な関数定義は効率が悪いのが通常で，そのままでは実用に供することができません． これを等式論証の手法を用いて，意味を変えずに，複雑ではあるけれど効率の良い定義を導出するのが，プログラム運算（program calculation）です． 最大切片和（maximum segment sum）問題 これは有名な問題で，与えられた整数列のすべての切片の和のうち最大のものを求めよ，というものです． 切片（segment）は，連
Refactoring with Equational Reasoning
Summary: Haskell is great for refactoring, thanks to being able to reason about and transform programs with confidence. I think one of Haskell's strengths as a practical language is that it's easy to refactor, and more importantly, easy to refactor safety. Programs in the real world often accumulate technical debt - code that is shaped more by its history than its current purpose. Refactoring is o
My Haskell tooling wishlist
I spend a lot of my time on Haskell tooling, both for my hobbies and my job. Almost every project I work on sparks a desire for another piece of tooling. Much of the time, I’ll follow that wish and take a detour to implement that thing (Fay, structured-haskell-mode, hindent, are some Haskell-specific examples). But in the end it means less time working on the actual domain problem I’m interested i
Equational reasoning at scale
Haskell programmers care about the correctness of their software and they specify correctness conditions in the form of equations that their code must satisfy. They can then verify the correctness of these equations using equational reasoning to prove that the abstractions they build are sound. To an outsider this might seem like a futile, academic exercise: proving the correctness of small abstra
Equational reasoning examples - HaskellWiki
One of the advantages often claimed for pure functional languages is the ease of equational reasoning, enabled by referential transparency and being able to replace equals by equals in all contexts. That is all great, and this page is not about repeating or elaborating on these things. But what, if anything, does it mean in programming practice? This page is about collecting (links to) examples of
Haskell for all: Equational reasoning
You may have heard that Haskell is "great for equational reasoning", but perhaps you didn't know precisely what that meant. This post will walk through an intermediate example of equational reasoning to show how you can interpret Haskell code by hand by applying substitutions as if your code were a mathematical expression. This process of interpreting code by substituting equals-for-equals is know
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
The Comonad.Reader » Internalized Guarded Recursion for Equational Reasoning
等式推論
http://www.cs.ox.ac.uk/jeremy.gibbons/publications/mr.pdf
Types for Programming and Reasoning