/Stefan

Mark

On 11 May, 19:21, snorgers <stefan.ta...@spray.se> wrote:

use the translate function on this page (see the example at the
bottom)

On the top forum page to the right you have the pages tab

Click that and you can add a new subject page. You will enter a
WYSIWYG kind of widget. there also is a html button on the bottom
of that page, click there and paste the generated html, enclose it in
<pre></pre> and publish it

/Stefan

On 11 May, 21:39, Mark Tarver <dr.mtar...@ukonline.co.uk> wrote:

WRITE-CHAR: argument |;| is not a character

when you run it.  It looks as if you put ; as a symbol onto a stream
that is supposed to be a stream/list of characters.

Mark
On 11 May, 22:00, snorgers <stefan.ta...@spray.se> wrote:

Mark

On 12 May, 17:37, snorgers <stefan.ta...@spray.se> wrote:

Its cute - do you think it might work even better if my comments were
black and italicised?

Mark

<PRE> <FONT COLOR="#800000">\Some time back there was some discussion
wrt Qi and Coq and such. I wrote

QUOTE
But the basic idea is that in CTT (constructive type theory), rather
than have a program which is then type checked, you have a type and
then find a program to fit.  In other words, a problem is less of the
form 'Find a type for the following expression E', more of 'Here is a
type T, find an expression that inhabits it'.

Now generally the latter question is not very useful for programmers.
However it turns out that if you feed your type theory steroids, you
can cause it to beef up to the point where your type T *expresses a
formal specification of what the program is supposed to do.* The catch
however is that your 'roided-up' type theory is combinatorially
uncontrollable.  You cannot simply release your type checker on it.
So you have to interact with the type checker to derive the solution.
At that point you have to build a proof assistant and so you have your
NuPrls and Coqs etc.
UNQUOTE

I thought I might show you how to do CTT in Qi in a series of
occasional posts.  You need to load in the proof assistant in Qi
Programs/Chap15 that comes in the Qi download.  Its documented in
http://www.lambdassociates.org/Book/page311.htm.

If we're not bothered overmuch by type security we can build a fast
implementation using rule abstractions (see http://www.lambdassociates.org/Book/page306.htm
and after for how to work them).  A rule abstraction works on a list
of ordered pairs (sequent) &lt;A, C&gt; where A is a list of
assumption and B a conclusion.\</FONT>

<FONT COLOR="#ff950e">Qi</FONT> <FONT COLOR="#ff950e">II</FONT> 2008,
<FONT COLOR="#ff950e">Copyright</FONT> (<FONT COLOR="#ff950e">C</
FONT>) 2001-2008 <FONT COLOR="#ff950e">Mark</FONT> <FONT
COLOR="#ff950e">Tarver</FONT>
www.lambdassociates.org
<FONT COLOR="#9966cc">version</FONT> 1.06

<FONT COLOR="#800000">\Generally a starting point is the typed lambda
calculus which is part of Qi type theory and just about every typed
language.   I'm going to be brutal here to save space by saying
anything is a wff. \</FONT>

(0-) (<FONT COLOR="#9966cc">datatype</FONT> wff

        ____________
        <FONT COLOR="#ff950e">X</FONT> : wff;)

(1-) (<FONT COLOR="#9966cc">synonyms</FONT> sequent ([wff] <FONT
COLOR="#9966cc">*</FONT> wff))
<FONT COLOR="#9966cc">synonyms</FONT>

(2-) (<FONT COLOR="#9966cc">tc</FONT> <FONT COLOR="#9966cc">+</FONT>)
true

(3+) (<FONT COLOR="#5e11a6">define</FONT> abs
        {[sequent] --&gt; [sequent]}
        <FONT COLOR="#ff950e">S</FONT> -&gt; ((<FONT
COLOR="#9966cc">rule</FONT> <FONT COLOR="#ff950e">X</FONT> : <FONT
COLOR="#ff950e">A</FONT> &gt;&gt; <FONT COLOR="#ff950e">Y</FONT> :
<FONT COLOR="#ff950e">B</FONT>;
              ______________________
              (<FONT COLOR="#0000ff">/.</FONT> <FONT
COLOR="#ff950e">X</FONT> <FONT COLOR="#ff950e">Y</FONT>) : (<FONT
COLOR="#ff950e">A</FONT> --&gt; <FONT COLOR="#ff950e">B</FONT>);)
<FONT COLOR="#ff950e">S</FONT>))
abs : ((<FONT COLOR="#9966cc">list</FONT> ((<FONT
COLOR="#9966cc">list</FONT> wff) <FONT COLOR="#9966cc">*</FONT> wff))
--&gt; (<FONT COLOR="#9966cc">list</FONT> ((<FONT
COLOR="#9966cc">list</FONT> wff) <FONT COLOR="#9966cc">*</FONT> wff)))

(4+) (<FONT COLOR="#5e11a6">define</FONT> app
       {[sequent] --&gt; [sequent]}
        <FONT COLOR="#ff950e">S</FONT> -&gt; ((<FONT
COLOR="#9966cc">rule</FONT> <FONT COLOR="#ff950e">X</FONT> : (<FONT
COLOR="#ff950e">A</FONT> --&gt; <FONT COLOR="#ff950e">B</FONT>); <FONT
COLOR="#ff950e">Y</FONT> : <FONT COLOR="#ff950e">A</FONT>;
              ___________________________
              (<FONT COLOR="#ff950e">X</FONT> <FONT COLOR="#ff950e">Y</
FONT>) : <FONT COLOR="#ff950e">B</FONT>;) <FONT COLOR="#ff950e">S</
FONT>))
app : ((<FONT COLOR="#9966cc">list</FONT> ((<FONT
COLOR="#9966cc">list</FONT> wff) <FONT COLOR="#9966cc">*</FONT> wff))
--&gt; (<FONT COLOR="#9966cc">list</FONT> ((<FONT
COLOR="#9966cc">list</FONT> wff) <FONT COLOR="#9966cc">*</FONT> wff)))

(5+) (<FONT COLOR="#5e11a6">define</FONT> hyp
       {[sequent] --&gt; [sequent]}
       <FONT COLOR="#ff950e">S</FONT> -&gt; ((<FONT
COLOR="#9966cc">rule</FONT> _______________
                   <FONT COLOR="#ff950e">P</FONT> &gt;&gt; <FONT
COLOR="#ff950e">P</FONT>;) <FONT COLOR="#ff950e">S</FONT>))
hyp : ((<FONT COLOR="#9966cc">list</FONT> ((<FONT
COLOR="#9966cc">list</FONT> wff) <FONT COLOR="#9966cc">*</FONT> wff))
--&gt; (<FONT COLOR="#9966cc">list</FONT> ((<FONT
COLOR="#9966cc">list</FONT> wff) <FONT COLOR="#9966cc">*</FONT> wff)))

<FONT COLOR="#800000">\Here's a slightly odd def.  You'll see why its
useful in a bit.\</FONT>

(6+) (<FONT COLOR="#5e11a6">define</FONT> answer
       {[sequent] --&gt; [sequent]}
        [(<FONT COLOR="#9966cc">@p</FONT> <FONT COLOR="#ff950e">A</
FONT> <FONT COLOR="#ff950e">C</FONT>) | <FONT COLOR="#ff950e">S</
FONT>] -&gt; [(<FONT COLOR="#9966cc">@p</FONT> <FONT
COLOR="#ff950e">A</FONT> <FONT COLOR="#ff950e">C</FONT>) (<FONT
COLOR="#9966cc">@p</FONT> [<FONT COLOR="#ff950e">C</FONT> | <FONT
COLOR="#ff950e">A</FONT>] <FONT COLOR="#ff950e">C</FONT>) | <FONT
COLOR="#ff950e">S</FONT>])
answer : ((<FONT COLOR="#9966cc">list</FONT> ((<FONT
COLOR="#9966cc">list</FONT> wff) <FONT COLOR="#9966cc">*</FONT> wff))
--&gt; (<FONT COLOR="#9966cc">list</FONT> ((<FONT
COLOR="#9966cc">list</FONT> wff) <FONT COLOR="#9966cc">*</FONT> wff)))

<FONT COLOR="#800000">\Load the proof assistant\</FONT>

(6+) (<FONT COLOR="#9966cc">load</FONT> <FONT COLOR="#b3b300">"../Qi
Programs/Chap15/proof assistant.qi"</FONT>)
.....................
loaded : <FONT COLOR="#99ccff">symbol</FONT>

<FONT COLOR="#ff950e">Off</FONT> we go.

(16+) (proof-assistant _)

<FONT COLOR="#ff950e">Input</FONT> assumptions?  (y/n) n

<FONT COLOR="#ff950e">Enter</FONT> conclusion: [[<FONT
COLOR="#0000ff">/.</FONT> x x] : [a --&gt; a]]
==============================
<FONT COLOR="#ff950e">Step</FONT> 1          unsolved 1

?- [[<FONT COLOR="#0000ff">/.</FONT> x x] |:| [a --&gt; a]]

<FONT COLOR="#ff950e">Tactic:</FONT> abs
==============================
<FONT COLOR="#ff950e">Step</FONT> 2          unsolved 1

?- [x |:| a]

1. [x |:| a]

<FONT COLOR="#ff950e">Tactic:</FONT> hyp
<FONT COLOR="#ff950e">Real</FONT> time: 7.59375 sec.
<FONT COLOR="#ff950e">Run</FONT> time: 0.0 sec.
<FONT COLOR="#ff950e">Space:</FONT> 35360 <FONT COLOR="#ff950e">Bytes</
FONT>
proved : <FONT COLOR="#99ccff">symbol</FONT>

<FONT COLOR="#800000">\The *proof signature* of this proof is:

&gt;&gt; [[/. x x] |:| [a --&gt; a]], abs, hyp

OK so far? Now rule closures use unification.  So we can drive the
proof in different ways.  We can ask.

What is the type of [/. x x]?
What function inhabits [a --&gt; a]?

The latter question brings us closer to CTT.  Lets do it.\</FONT>

(21+) (proof-assistant _)

<FONT COLOR="#ff950e">Input</FONT> assumptions?  (y/n) n

<FONT COLOR="#ff950e">Enter</FONT> conclusion: [<FONT
COLOR="#ff950e">What?</FONT> : [a --&gt; a]]
==============================
<FONT COLOR="#ff950e">Step</FONT> 1          unsolved 1

?- [<FONT COLOR="#ff950e">What?</FONT> |:| [a --&gt; a]]

<FONT COLOR="#ff950e">Tactic:</FONT> answer
==============================
<FONT COLOR="#ff950e">Step</FONT> 2          unsolved 2

?- [<FONT COLOR="#ff950e">What?</FONT> |:| [a --&gt; a]]

<FONT COLOR="#ff950e">Tactic:</FONT> abs
==============================
<FONT COLOR="#ff950e">Step</FONT> 3          unsolved 2

?- [#:X16870 |:| a]

1. [#:X16867 |:| a]

<FONT COLOR="#ff950e">Tactic:</FONT> hyp
==============================
<FONT COLOR="#ff950e">Step</FONT> 4          unsolved 1

?- [[<FONT COLOR="#0000ff">/.</FONT> #:X16867 #:X16867] |:| [a --&gt;
a]]

1. [[<FONT COLOR="#0000ff">/.</FONT> #:X16867 #:X16867] |:| [a --&gt;
a]]

<FONT COLOR="#ff950e">Tactic:</FONT> hyp
<FONT COLOR="#ff950e">Real</FONT> time: 17.640625 sec.
<FONT COLOR="#ff950e">Run</FONT> time: 0.015625 sec.
<FONT COLOR="#ff950e">Space:</FONT> 76452 <FONT COLOR="#ff950e">Bytes</
FONT>
proved : <FONT COLOR="#99ccff">symbol</FONT>

<FONT COLOR="#800000">\The final sequent gives the answer.

Any legal substitution for the variables in [/. #:X16867 #:X16867] has
type [a --&gt; a].  The purpose of the answer function was to allow
this information to be displayed at the end of the proof.  We could
also ask our program to find a most general type for [/. x x].

This ability to synthesise a program (= lambda function) from a type
is the very beginning of CTT.  I leave you to play with this.

Mark\</FONT>

</PRE>

On 12 May, 17:37, snorgers <stefan.ta...@spray.se> wrote:

I will, my intention was to mix text and code and therefore it can
be good to leave the "pre" stuff out of it but I will add your
suggestion

/Stefan

On 12 May, 20:14, Mark Tarver <dr.mtar...@ukonline.co.uk> wrote:

-Al

/Stefan

I'll put this program into the library against your name.

Mark

On 12 May, 22:40, snorgers <stefan.ta...@spray.se> wrote:

/Stefan

I missed a reference to Mark
/Stefan

/Stefan