(original) (raw)

����;� TeX output 2005.06.22:1812����������2���7 �color push Black��� color pop�������x�������color push Black� color pop�������color push rgb 1 0 0�KtEo�1lcmss8�BEYOND�KkLISP� color pop������c�John�KkMcCa��O rthy���#,�Stanfo�rd�Universit�y����̼]Stanfo��O rd�KkJune�22,�2005������bhttp://www-fo��O rmal.stanfo�rd.edu/jmc/�����&jmc@cs.stanfo��O rd.edu�������color push rgb 1 0 0MAIN�KkPOINTS� color pop��8� ��7 ��K� �1cmsy8��Kk�Lisp�p��O rograms�a�re�Lisp�data|abstract�syntax.����7 Programming�`;languages�need�functions�fo��O r�their�abstract�syntax.����7 ��Kk�English�is�imp���o��O rtant�fo�r�its�semantics|not�its�syntax����7 ��Kk�The�la��O rgest�piece�of�cak�e|Kleene���2�1cmmi8���op���erato�r����7 ��Kk�An�elephant�never�fo��O rgets�and�is�faithful.����7 ��Kk�Resolution�considered�ha��O rmful.����7 ��Kk�Sp���ecial�p��O rovers�a�re�just�strategies|Davis-Putnam����7 ��Kk�Programs�as�logical�fo��O rmulas|Algol�48�and�Algol�50�����7 �color push Black���V,��KtEo ��lcmss8�1����� color pop����*�����2���7 �color push Black��� color pop�������x����A_��color push Black� color pop���K_��color push rgb 1 0 0�PROGRAMS�KkAS�D��O A���#T�A|ABSTRA�CT�KkSYNT�AX� color pop��-�B��7 ��Kk�Sums�ma��O y�b���e�rep�resented�as�(+�x�y),�x�+�y���#,�3����y��2� cmmi8�x�� l$�7����y�y��B�as�text.��-��7 ��Kk�issum�(�exp�),��s�1(�exp�),��s�2(�exp�),��mk���sum�(�exp�1�;��vexp�2)����7 �� ��Programming�languages�(even�Java�and�Curl)�need�their�ab-��ލ�7 stract��syntaxes�de ned�and�function�in�the�language�fo��O r�the�ab-����7 stract�Kksyntax.��-��7 ��Kk�Lisp�is�close�to�its�abstract�syntax,�but�needs�it�anyw��O a�y���#.����7 ���Y�Input�syntax,� �p��O rint�syntax,�compute�with�it�syntax.� �޼x�9�+�3,���color push rgb 1 0 0�x���� color pop��color push rgb 0 0 1�+��Z�� color pop3,��ލ�7 (+�Kkx�3).� 9���1lcmssi8�I�should�have�given�the�list�structure.����7 ��Kk�issubr��ioutine�(�exp�),��body��ع(�exp�),��isj�%�av�apr��iog�r�am�(�exp�)����7 ��Kk�http://www-fo��O rmal.stanfo�rd.edu/jmc/to�w�a�rds.html�(1962)�����7 �color push Black���V,»2����� color pop����y�����2���7 �color push Black��� color pop�������x���� t{�color push Black� color pop���t{�color push rgb 1 0 0�ENGLISH�KkAS�A�PROGRAMMING�LANGUA��O GE|IT'S�THE������`SEMANTICS�KkTHA���#T'S�IMPORT�ANT� color pop��1�d��7 ��ȑ�COBOL:�add�3�to�x,���F��O ORTRAN:�x�=�x�+�3,�Algol�60:� �x�:=����7 x�Kk+�3;�trivial�va��O riants��:��7 ��Kk�\the�la��O rgest�piece�of�cak�e",�Kleene����op���erato�r����7 �����\I��Uneed�to�b���e�at�a�meeting�in�Monterrey���#,���Mexico�from�Novem-����7 b���er�Kk15�to�17"�follo��O w�ed�Kkb�y�dialog�ab���out�details.����7 ���ֹ\The�U.S.�w��O ants�Iraq�to�b���ecome�a�non-aggressive,�&'p�rosp���erous,����7 demo���cracy"|Plan� �government�p�olicy���#.� 6[to�b�e�done�without�a����7 p��O recise�Kkde nition�of�demo���cracy].�����7 �color push Black���V,»3����� color pop���� �����2���7 �color push Black��� color pop�������x����ZB�color push Black� color pop���dB�color push rgb 1 0 0�INCLUDE�KkLOGICAL�SENTENCES�IN�LISP� color pop��1�d��7 �����(assert�`(on�blo���ck1�,x)),�-(assert�'((fo��O rall�b�o��O y)((exists�girl)((loves����7 girl�Kk(only�b���o��O y))))))��:��7 ��Kk�Also�include�a�theo��O rem�p�rover-p�roblem�solver����7 ��Kk�Resolution�considered�ha��O rmful.����7 �� �p�Sp���ecial�p��O rovers�a�re�just�tactics�in�general�p�rovers�to�b���e�used����7 on� �zsubp��O roblems,� f>e.g.�gDavis-Putnam�used�when�only�the�outer����7 p��O rop���ositional��structure�is�considered.� �G[�color push rgb 1 0 0confession:� color pop� yNI�Hcan't�do�this����7 y��O et.�����7 �color push Black���V,»4����� color pop���� ������2���7 �color push Black��� color pop�������x��������color push Black� color pop������color push rgb 1 0 0�ELEPHANT� color pop��1�d��7 ��Kk�Elephants�never�fo��O rget.� 9An�elephant�is�faithful,�100�p���ercent.��:��7 ��I¹A�I�passenger�has�a�reservation�if�he�has�made�one�and�it�hasn't����7 b���een� ��cancelled.�3PP��O assengers�with�reservations�should�b�e�on�the����7 passenger�Kklist�at� ight�time.����7 ���¹A��necessa��O ry�condition�fo�r�p�rogram�co�rrectness�is�that�a�p�rogram����7 ful ll�Kkits�p��O romises.����7 ��Kk�Alas,�Elephant�2000�is�not�ready�to�b���e�implemented.����7 ��Kk�http://www-fo��O rmal.stanfo�rd.edu/jmc/elephant.html�����7 �color push Black���V,»5����� color pop���������2���7 �color push Black��� color pop�������~p��������color push Black� color pop��� ���color push rgb 1 0 0�ALGOL�Kk48� color pop��1�d��7 If� hBw��O e�intro���duce�time�explicitly�as�distinct�from�the�p�rogram����7 counter,� -�Algolic� �Bp��O rograms�can�b���e�written�as�sets�of�equations.����7 Here's� u�an�Algol�60�p��O rogram�fo�r�computing�the�p�ro���duct��mn��of����7 t��O w�o�Kknatural�numb���ers.��+������ �star��it���:��������՞�i����� "�:=�����MK�n�;��������cv�p����� "�:=�����MK0;�����������l�<soop���:�����mk�if� }<i���="�0�Kk�then�g����o�to�done�;���������՞�i������" "�:="�����MK�i��H����1;����������+��g����oto�����MKl�<soop�;����������~��done���:���������7" �color="" push="" black���v,»6�������="" color="" pop����������������������������������������������������2�����7="" black�����="" pop���������x����7="" �here's��_what�mathematicians�might�have�written�in�1948,��ab����efo��o re������7="" p��o rogramming�kklanguages�existed.��+������z�="">�pc�(0)������-�=��������0;��������B��i�(�t��H�+�1)������-�=���������if�����pc�(�t�)��=�0��Kkthen��=���n���������7 �else�Kkif��C��pc�(�t�)��=�4����then��E��i�(�t�)��H���1��Kkelse��5�ռi�(�t�);��������?W�p�(�t��H�+�1)������-�=���������if�����pc�(�t�)��=�1��Kkthen��=��0����������else�Kkif��E�~�pc�(�t�)��=�5��Kkthen��=���p�(�t�)��H+��m��Kk�else��5�ռp�(�t�)��������6.��pc�(�t��H�+�1)������-�=���������if�����pc�(�t�)��=�2��H�^��i�(�t�)��=�0��Kkthen��=��6����������Kelse�Kkif��Q�8�pc�(�t�)��=�5��Kkthen��=��2��Kkelse��5�ռpc�(�t�)��H+�1;������������color push Black(1)� color pop�������7 �color push Black��� color pop����Q�����2���7 �color push Black��� color pop�������؞��7 �The� ڪp��O ro���of�that��9�t:�(�t�����0����^��pc�(�t�)��=�6����^��p�(�t�)��=��mn�)� ڪfollo�ws�from����7 the��#sentences�exp��O ressing�the�p�rogram�and�the�la�ws�of�a�rithmetic,����7 i.e.���no� �0theo��O ry�of�p�rogram�co�rrectness�is�needed.���Ho�w�ever,� ��the����7 p��O ro���of�7�ideas�a�re�essentially�the�same�as�those�used�to�p�rove�that����7 an� malgolic�p��O rogram�terminates�and�that�the�outputs�have�the����7 co��O rrect� :�relation�to�the�inputs.� ��Amir�Pnueli�and�Nissim�F�rancez����7 had��Kthis�idea�b���efo��O re�I��9did,��Cbut�they�mistak�enly�abandoned�it�fo�r����7 temp���o��O ral�Kklogic.�����7 �color push Black��� color pop����������2���7 �color push Black��� color pop�������x����c���color push Black� color pop���m���color push rgb 1 0 0�PRO��O VING�KkLISP�PROGRAMS�CORRECT� color pop�����7 �color push Black���V,»7����� color pop�������;���7  ���1lcmssi8��K� �1cmsy8��2� cmmi8��2�1cmmi8�KtEo ��lcmss8�KtEo�1lcmss8�1������</soop���:�����mk�if�>