| Newsgroups |
gmane.comp.lang.concatenative |
| Message-ID |
<[email protected]> |
--dGwgNmomgOBMLSVEawyk-F4uH5tocWsDlnu7Zgs
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: quoted-printable
On Nov 6, 2014, at 12:20 PM, chris glur [email protected] [concatenative] <co=
[email protected]> wrote:
> Searching the literature in this direction I came across repeated claims
> that certain functional languages could formally prove correctness via
> algebraic manipulation of the code.
There are more than just claims, you'll be happy to know!
Richard Bird and Jeremy Gibbons have done a lot of work on this topic. Bird=
's "The Algebra of Programming" is possibly the best book to pick up, but i=
t can be hard to find for a sane price. This paper by Gibbons appears to be=
a good proxy:
http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-calcfp.pdf
If you've not read it yet, you should also read Backus's famous paper for s=
ome of the origins of the idea of calculating programs:
http://web.stanford.edu/class/cs242/readings/backus.pdf
I'd also look at categorical programming languages like Charity. The paper =
you want to read is called "Charitable Thoughts", but it may be hard to fin=
d in the sea of academic FTP wastelands. If you can't dig it up somewhere, =
let me know and I'll send you a copy. (I can't at the moment due to being a=
t work.) You can also look at Hagino's thesis on the topic:
http://synrc.com/publications/cat/Category%20Theory/Type%20Theory/Hagino%20=
T.%20A%20Categorical%20Programming%20Language.pdf
Of course, if you really want to prove non-trivial things (e.g. "my red-bla=
ck tree implementation is actually self-balancing"), you're not going to be=
doing it algebraically. You're going to be using constructive proofs and a=
language like Coq. If you want to learn more about how to do such proofs, =
read this book by Adam Chlipala:
http://adam.chlipala.net/cpdt/
If you're serious about wanting to prove things formally, the tools are alr=
eady there. Go use them and show us all your cool stuff!
> Several examples of manipulating the code of the language: joy; were publ=
ished, but I never saw a complete task being proved.
In my humble opinion, concatenative languages are not great for algebraic m=
anipulation. The problem is that the stack is threaded through every functi=
on (more or less), and this makes it very difficult to reason about things =
in isolation.
If you want a concrete example of the problem, try writing a version of the=
'map' function in Joy such that it has the following semantics; you'll see=
it's not as easy as it looks:
forall F G. [F] map [G] map =3D=3D [F G] map
(Someone may object to this example because 'map' in a concatenative langua=
ge is typically equivalent to a combination of 'map' and 'fold'. Given that=
the accumulator passed to such a map/fold is the *entire state of the prog=
ram*, I hardly think this makes things better!)=20
- jn
--dGwgNmomgOBMLSVEawyk-F4uH5tocWsDlnu7Zgs
Content-Type: text/html; charset=US-ASCII
Content-Transfer-Encoding: 7bit
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
<html>
<head>
</head>
<body style="background-color: #fff;">
<span style="display:none"> </span>
<!--~-|**|PrettyHtmlStartT|**|-~-->
<div id="ygrp-mlmsg" style="position:relative;">
<div id="ygrp-msg" style="z-index: 1;">
<!--~-|**|PrettyHtmlEndT|**|-~-->
<div id="ygrp-text" >
<p>On Nov 6, 2014, at 12:20 PM, chris glur [email protected] [concatenative] <[email protected]> wrote:<br>
<br>
> Searching the literature in this direction I came across repeated claims<br>
> that certain functional languages could formally prove correctness via<br>
> algebraic manipulation of the code.<br>
<br>
There are more than just claims, you'll be happy to know!<br>
<br>
Richard Bird and Jeremy Gibbons have done a lot of work on this topic. Bird's "The Algebra of Programming" is possibly the best book to pick up, but it can be hard to find for a sane price. This paper by Gibbons appears to be a good proxy:<br>
<br>
http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-calcfp.pdf<br>
<br>
If you've not read it yet, you should also read Backus's famous paper for some of the origins of the idea of calculating programs:<br>
<br>
http://web.stanford.edu/class/cs242/readings/backus.pdf<br>
<br>
I'd also look at categorical programming languages like Charity. The paper you want to read is called "Charitable Thoughts", but it may be hard to find in the sea of academic FTP wastelands. If you can't dig it up somewhere, let me know and I'll send you a copy. (I can't at the moment due to being at work.) You can also look at Hagino's thesis on the topic:<br>
<br>
http://synrc.com/publications/cat/Category%20Theory/Type%20Theory/Hagino%20T.%20A%20Categorical%20Programming%20Language.pdf<br>
<br>
Of course, if you really want to prove non-trivial things (e.g. "my red-black tree implementation is actually self-balancing"), you're not going to be doing it algebraically. You're going to be using constructive proofs and a language like Coq. If you want to learn more about how to do such proofs, read this book by Adam Chlipala:<br>
<br>
http://adam.chlipala.net/cpdt/<br>
<br>
If you're serious about wanting to prove things formally, the tools are already there. Go use them and show us all your cool stuff!<br>
<br>
> Several examples of manipulating the code of the language: joy; were published, but I never saw a complete task being proved.<br>
<br>
In my humble opinion, concatenative languages are not great for algebraic manipulation. The problem is that the stack is threaded through every function (more or less), and this makes it very difficult to reason about things in isolation.<br>
<br>
If you want a concrete example of the problem, try writing a version of the 'map' function in Joy such that it has the following semantics; you'll see it's not as easy as it looks:<br>
<br>
forall F G. [F] map [G] map == [F G] map<br>
<br>
(Someone may object to this example because 'map' in a concatenative language is typically equivalent to a combination of 'map' and 'fold'. Given that the accumulator passed to such a map/fold is the *entire state of the program*, I hardly think this makes things better!) <br>
<br>
- jn</p>
</div>
<!--~-|**|PrettyHtmlStart|**|-~-->
<div style="color: #fff; height: 0;">__._,_.___</div>
<div style="clear:both"> </div>
<div id="fromDMARC" style="margin-top: 10px;">
<hr style="height:2px ; border-width:0; color:#E3E3E3; background-color:#E3E3E3;">
Posted by: John Nowak <[email protected]> <hr style="height:2px ; border-width:0; color:#E3E3E3; background-color:#E3E3E3;">
</div>
<div style="clear:both"> </div>
<table cellspacing=4px style="margin-top: 10px; margin-bottom: 10px; color: #2D50FD;">
<tbody>
<tr>
<td style="font-size: 12px; font-family: arial; font-weight: bold; padding: 7px 5px 5px;" >
<a style="text-decoration: none; color: #2D50FD" href="https://groups.yahoo.com/neo/groups/concatenative/conversations/messages/5023;_ylc=X3oDMTJwZmw2MWtnBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BG1zZ0lkAzUwMjMEc2VjA2Z0cgRzbGsDcnBseQRzdGltZQMxNDE2MzI4NDcy?act=reply&messageNum=5023">Reply via web post</a>
</td>
<td>•</td>
<td style="font-size: 12px; font-family: arial; padding: 7px 5px 5px;" >
<a href="mailto:[email protected]?subject=Re%3A%20%5Bstack%5D%20Formal%20proofs%20via%20%27joy%27%20or%20any%20system%3F" style="text-decoration: none; color: #2D50FD;">
Reply to sender </a>
</td>
<td>•</td>
<td style="font-size: 12px; font-family: arial; padding: 7px 5px 5px;">
<a href="mailto:[email protected]?subject=Re%3A%20%5Bstack%5D%20Formal%20proofs%20via%20%27joy%27%20or%20any%20system%3F" style="text-decoration: none; color: #2D50FD">
Reply to group </a>
</td>
<td>•</td>
<td style="font-size: 12px; font-family: arial; padding: 7px 5px 5px;" >
<a href="https://groups.yahoo.com/neo/groups/concatenative/conversations/newtopic;_ylc=X3oDMTJldGVyN2ZiBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA250cGMEc3RpbWUDMTQxNjMyODQ3Mg--" style="text-decoration: none; color: #2D50FD">Start a New Topic</a>
</td>
<td>•</td>
<td style="font-size: 12px; font-family: arial; padding: 7px 5px 5px;color: #2D50FD;" >
<a href="https://groups.yahoo.com/neo/groups/concatenative/conversations/topics/5022;_ylc=X3oDMTM0cmZibDF1BF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BG1zZ0lkAzUwMjMEc2VjA2Z0cgRzbGsDdnRwYwRzdGltZQMxNDE2MzI4NDcyBHRwY0lkAzUwMjI-" style="text-decoration: none; color: #2D50FD;">Messages in this topic</a>
(2)
</td>
</tr>
</tbody>
</table>
<!------- Start Nav Bar ------>
<!-- |**|begin egp html banner|**| -->
<div id="ygrp-vital" style="background-color: #f2f2f2; font-family: Verdana; font-size: 10px; margin-bottom: 10px; padding: 10px;">
<span id="vithd" style="font-weight: bold; color: #333; text-transform: uppercase; "><a href="https://groups.yahoo.com/neo/groups/concatenative/info;_ylc=X3oDMTJlN3RuMXY5BF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwN2dGwEc2xrA3ZnaHAEc3RpbWUDMTQxNjMyODQ3Mg--" style="text-decoration: none;">Visit Your Group</a></span>
<ul style="list-style-type: none; margin: 0; padding: 0; display: inline;">
</ul>
</div>
<div id="ft" style="font-family: Arial; font-size: 11px; margin-top: 5px; padding: 0 2px 0 0; clear: both;">
<a href="https://groups.yahoo.com/neo;_ylc=X3oDMTJkcm5tdmw4BF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA2dmcARzdGltZQMxNDE2MzI4NDcy" style="float: left;"><img src="http://l.yimg.com/ru/static/images/yg/img/email/new_logo/logo-groups-137x15.png" height="15" width="137" alt="Yahoo! Groups" style="border: 0;"/></a>
<div style="color: #747575; float: right;"> • <a href="https://info.yahoo.com/privacy/us/yahoo/groups/details.html" style="text-decoration: none;">Privacy</a> • <a href="mailto:[email protected]?subject=Unsubscribe" style="text-decoration: none;">Unsubscribe</a> • <a href="https://info.yahoo.com/legal/us/yahoo/utos/terms/" style="text-decoration: none;">Terms of Use</a> </div>
</div>
<br>
<!-- |**|end egp html banner|**| -->
</div> <!-- ygrp-msg -->
<!-- Sponsor -->
<!-- |**|begin egp html banner|**| -->
<div id="ygrp-sponsor" style="width:160px; float:right; clear:none; margin:0 0 25px 0; background: #fff;">
<!-- Start Recommendations -->
<div id="ygrp-reco">
</div>
<!-- End Recommendations -->
</div> <!-- |**|end egp html banner|**| -->
<div style="clear:both; color: #FFF; font-size:1px;">.</div>
</div>
<img src="http://geo.yahoo.com/serv?s=97359714/grpId=1839274/grpspId=1705006764/msgId=5023/stime=1416328472" width="1" height="1"> <br>
<img src="http://y.analytics.yahoo.com/fpc.pl?ywarid=515FB27823A7407E&a=10001310322279&js=no&resp=img" width="1" height="1">
<div style="color: #fff; height: 0;">__,_._,___</div>
<!--~-|**|PrettyHtmlEnd|**|-~-->
</body>
<!--~-|**|PrettyHtmlStart|**|-~-->
<head>
<style type="text/css">
<!--
#ygrp-mkp {
border: 1px solid #d8d8d8;
font-family: Arial;
margin: 10px 0;
padding: 0 10px;
}
#ygrp-mkp hr {
border: 1px solid #d8d8d8;
}
#ygrp-mkp #hd {
color: #628c2a;
font-size: 85%;
font-weight: 700;
line-height: 122%;
margin: 10px 0;
}
#ygrp-mkp #ads {
margin-bottom: 10px;
}
#ygrp-mkp .ad {
padding: 0 0;
}
#ygrp-mkp .ad p {
margin: 0;
}
#ygrp-mkp .ad a {
color: #0000ff;
text-decoration: none;
}
#ygrp-sponsor #ygrp-lc {
font-family: Arial;
}
#ygrp-sponsor #ygrp-lc #hd {
margin: 10px 0px;
font-weight: 700;
font-size: 78%;
line-height: 122%;
}
#ygrp-sponsor #ygrp-lc .ad {
margin-bottom: 10px;
padding: 0 0;
}
#actions {
font-family: Verdana;
font-size: 11px;
padding: 10px 0;
}
#activity {
background-color: #e0ecee;
float: left;
font-family: Verdana;
font-size: 10px;
padding: 10px;
}
#activity span {
font-weight: 700;
}
#activity span:first-child {
text-transform: uppercase;
}
#activity span a {
color: #5085b6;
text-decoration: none;
}
#activity span span {
color: #ff7900;
}
#activity span .underline {
text-decoration: underline;
}
.attach {
clear: both;
display: table;
font-family: Arial;
font-size: 12px;
padding: 10px 0;
width: 400px;
}
.attach div a {
text-decoration: none;
}
.attach img {
border: none;
padding-right: 5px;
}
.attach label {
display: block;
margin-bottom: 5px;
}
.attach label a {
text-decoration: none;
}
blockquote {
margin: 0 0 0 4px;
}
.bold {
font-family: Arial;
font-size: 13px;
font-weight: 700;
}
.bold a {
text-decoration: none;
}
dd.last p a {
font-family: Verdana;
font-weight: 700;
}
dd.last p span {
margin-right: 10px;
font-family: Verdana;
font-weight: 700;
}
dd.last p span.yshortcuts {
margin-right: 0;
}
div.attach-table div div a {
text-decoration: none;
}
div.attach-table {
width: 400px;
}
div.file-title a, div.file-title a:active, div.file-title a:hover, div.file-title a:visited {
text-decoration: none;
}
div.photo-title a, div.photo-title a:active, div.photo-title a:hover, div.photo-title a:visited {
text-decoration: none;
}
div#ygrp-mlmsg #ygrp-msg p a span.yshortcuts {
font-family: Verdana;
font-size: 10px;
font-weight: normal;
}
.green {
color: #628c2a;
}
.MsoNormal {
margin: 0 0 0 0;
}
o {
font-size: 0;
}
#photos div {
float: left;
width: 72px;
}
#photos div div {
border: 1px solid #666666;
height: 62px;
overflow: hidden;
width: 62px;
}
#photos div label {
color: #666666;
font-size: 10px;
overflow: hidden;
text-align: center;
white-space: nowrap;
width: 64px;
}
#reco-category {
font-size: 77%;
}
#reco-desc {
font-size: 77%;
}
.replbq {
margin: 4px;
}
#ygrp-actbar div a:first-child {
/* border-right: 0px solid #000;*/
margin-right: 2px;
padding-right: 5px;
}
#ygrp-mlmsg {
font-size: 13px;
font-family: Arial, helvetica,clean, sans-serif;
*font-size: small;
*font: x-small;
}
#ygrp-mlmsg table {
font-size: inherit;
font: 100%;
}
#ygrp-mlmsg select, input, textarea {
font: 99% Arial, Helvetica, clean, sans-serif;
}
#ygrp-mlmsg pre, code {
font:115% monospace;
*font-size:100%;
}
#ygrp-mlmsg * {
line-height: 1.22em;
}
#ygrp-mlmsg #logo {
padding-bottom: 10px;
}
#ygrp-msg p a {
font-family: Verdana;
}
#ygrp-msg p#attach-count span {
color: #1E66AE;
font-weight: 700;
}
#ygrp-reco #reco-head {
color: #ff7900;
font-weight: 700;
}
#ygrp-reco {
margin-bottom: 20px;
padding: 0px;
}
#ygrp-sponsor #ov li a {
font-size: 130%;
text-decoration: none;
}
#ygrp-sponsor #ov li {
font-size: 77%;
list-style-type: square;
padding: 6px 0;
}
#ygrp-sponsor #ov ul {
margin: 0;
padding: 0 0 0 8px;
}
#ygrp-text {
font-family: Georgia;
}
#ygrp-text p {
margin: 0 0 1em 0;
}
#ygrp-text tt {
font-size: 120%;
}
#ygrp-vital ul li:last-child {
border-right: none !important;
}
-->
</style>
</head>
<!--~-|**|PrettyHtmlEnd|**|-~-->
</html>
<!-- end group email -->
--dGwgNmomgOBMLSVEawyk-F4uH5tocWsDlnu7Zgs--