mizvekov wrote:Okay, I am a bit stumped on this one.

I'd expect you to be. I've thrown you in at the deep end wearing concrete shoes.

I think that I need axiom3 to prove it, and this axiom cannot be used implicitly from this proof language, so I need to instantiate it manually and then bring it into the proof by using the UseTheorem constructor.

Right. Actually, I've used the axiom twice with two different instantiations. Rather than doing the instantiation manually, you might find this function helps:

Code: Select all

-- matchMP ( Γ ⊢ (P → Q) (Δ ⊢ P') attempts to match P with P', and then applies MP.
matchMP :: Theorem String -> Proof -> Proof
matchMP imp ant =
  let antT = concl ant in
    case theoremTerm imp of
      p :=>: q ->
        case match p antT of
          [insts] -> MP (UseTheorem $ instM Var insts imp) ant
          _       -> error "MATCH MP"
      _ -> error "MATCH MP"

This function is like mp, but it will try to instantiate the second argument to make it line up with the first.

The reason I need it is because I need the following auxiliary theorems:
1) |- (~p -> ~q) -> (q -> p)
2) |- (~p -> q) -> (~q -> p)

Number 1 is easy to do with "instL [p, q] axiom3".
Now number 2 is hard. Maybe it's just my mind being burned out from making sense of all that code and then trying to solve this, but anyway, if I do "instL [p, Not q] axiom3" then I get "|- (~p ==> ~~q) ==> ~q ==> p", and so I still have that double negation, which I have to get rid of. So I would need a theorem like: "|- (p ==> q) ==> (p ==> ~~q)", and this last one I am not seeing how to prove...
Will give it another go tomorrow.

It might be that you are trying to prove something that is more aptly derived from the exercise theorem. Note though, that it took me 16 proof steps in all to do this.

VazScep wrote:Okay, but still I need to be able to prove that one with just these 3 axioms!

Yeah, there's a fair bit of work to go. My Bootstrap file is 425 lines of proof.

VazScep wrote:Yes, and I also remember that monads are another example of a combinator language, so I know I have used them, but I never tried implementing a new one yet.

Yes. In fact, I'd say that the monad combinators are an abstraction over various other combinator languages.

VazScep wrote:That irks me a bit. Perhaps I am being too naive here, but I think the universities place is to teach students how to think and learn for themselves, and not to focus too much on directly teaching trade skills.

Not sure. I'd struggle to be able to give a definition of computer science and what a computer science degree should entail. At one end, if it's just the professional degree of a programmer, then I guess they should be expected to learn as many trade skills as a mechanical engineer

VazScep wrote:I am not so sure here. I understand that haskell makes it a lot easier for someone who is trying to make a program and prove that it is bug free, but I am not so sure if it would significantly reduce the number of bugs when it's the joe average industry programmer. There is just a lot of bugs that the type system will not catch.

Heretic! If it types, it's correct!

Yeah, maybe there's more to this, or maybe less. I'm just trying to think of reasons why Common Lisp was made to be so dynamic.

VazScep wrote:I see. But then are these interpreter sessions secure? I mean I get the impression that whoever is using it could just do something similar to what I did and violate the encapsulation of the kernel.

Well, you can't pull that trick off in Ocaml. But you could always violate the encapsulation just by changing the kernel code.

The type of security here is more like self-assurance. I want to trust that I haven't violated encapsulation, and that the tools I write aren't cheating. If any tool, no matter how complex and opaque, manages to produce an object that types as a theorem, I have an extremely strong guarantee from the type system that it went through the kernel.

The sort of security I don't have is security from a malicious programmer, who perhaps used "Obj.magic" to circumvent the type system, or exploited a vulnerability in the Ocaml interpreter, or customised the pretty printer to render his trivial theorem that "1 + 1 = 2" as the statement of Fermat's Last Theorem.

I can imagine a world where we actually start paying people large sums of money to do significant formalisation work. We'll probably have to be more concerned then with cheaters.

Interesting post, epepke. Just a few comments:

epepke wrote:Jumping in here.

I learned LISP in my first semester at MIT. LISP was the Big Deal there at the time (late 1970s), and that's what they taught the frosh (now I hear they use Python, which is very LISP-like but with syntax). I had already learned BASIC (with line numbers), COBOL, Tutor (later renamed PAL), and Z-80 assembly.

LISP was very badly taught at MIT.

That's a shame. I assume by the 80s, things had improved substantially with Structure and Interpretations of Computer Programs. The book is brilliant, at least.

All the examples had unnecessary PROGs all over the place. The first example of recursion they gave was the Fibonacci sequence, which is bad, because the iterative solution is so obvious and obviously better.

Oh, I dunno. Once you have laziness, I think the recursive solution is stunning. If you take two copies of the Fibonacci sequence, chopping off the first element of one, you get:

1, 1, 2, 3, 5, 8, 13, ...
1, 2, 3, 5, 8, 13, 21, ...

Now if you apply addition vertically, you obviously get the Fibonacci sequence with two elements chopped off the front. In other words:

Code: Select all

fibs = 1 : 1 : zipWith (+) fibs (tail fibs)

Note that the way graph reduction is performed in a lazy language means that evaluation here has the same complexity as the iterative solution.

LISP is extremely beautiful. Common LISP, however, has so much stuff in it that it strikes me as extremely unwieldy. I cannot remember who, but somebody said that every significant implementation contains a bug-ridden implementation of about half of Common LISP. I think this is true. The internal ideas of LISP and the way it handles memory are quite good, and even in programs in C and C++, it makes a lot of sense to write something like LISP internally.

Is there really just one LISP? I read a series of early articles in the History of Programming Languages on this, and my understanding was that there were many dialects around for decades before CL.

VazScep wrote:I'm much more hopeful about F#, which has made far fewer concessions to the OO world and looks far more like an ML dialect.

F# is virtually the same as OCaml, which is my FP language of choice. (Haskell is just as impractical as all hell.)

Note that while OCaml's name implies object orientation, no one is forcing you to use the object system. The standard library, as far as I know, doesn't use it, and neither do a lot of major third party libraries, like ocamlgraph and Batteries. You can "subclass" certain modules with functors though.

VazScep wrote:If it makes sense to say, I find Common Lisp far too powerful.

In that the de facto standard runs over 1,000 pages, I guess CL is powerful in the sense that it has a lot of features but I never did understand people who think they're Jedi knights because they use it. CL is a bloated, ugly, design-by-committee language.

Sigillum Militum wrote:F# is virtually the same as OCaml, which is my FP language of choice. (Haskell is just as impractical as all hell.)

Is F# or Ocaml your language of choice? Either's awesome. Do you manage to use either in your professional work?

Note that while OCaml's name implies object orientation, no one is forcing you to use the object system. The standard library, as far as I know, doesn't use it, and neither do a lot of major third party libraries, like ocamlgraph and Batteries. You can "subclass" certain modules with functors though.

I'm not really sure what you're thinking of here.

There will be some overlap, because in languages like C# and Java, the class system is used for multiple purposes. It is used for single-dynamic-dispatch (a form of subtyping), which is something that Ocaml's modules cannot do. But it is also used for modular programming, which is something that Ocaml's modules can do, and can often do better.

For instance, suppose you want to abstract over a function which creates an object of abstract type t. In Ocaml/Standard ML, this is a completely natural thing to do, and is handled by having a signature declaring an abstract type "t" and a function "create_t" of a type with form ".. -> .. -> .. -> t".

In Java, I would need to abstract over constructors, which I can't do. So I end up with a more convoluted design involving two interfaces, one for the returned type and one for the constructing function (typically called an "abstract factory"). Yuck.

VazScep wrote:If it makes sense to say, I find Common Lisp far too powerful.

In that the de facto standard runs over 1,000 pages, I guess CL is powerful in the sense that it has a lot of features but I never did understand people who think they're Jedi knights because they use it. CL is a bloated, ugly, design-by-committee language.

It's too powerful in that I think it's too hackable. I suspect that is what leads to any Jedi Knight phenomenon, and the failure to realise that just because it's possible to hack some weird shit into CL, it doesn't mean it's a good idea.

In the end, most of the things that got me interested in CL were things that were done just as well if not better in statically typed functional languages. The only thing that left it unique were macros, whose utility I grossly overestimated.

VazScep wrote:Is F# or Ocaml your language of choice? Either's awesome. Do you manage to use either in your professional work?

OCaml and I do not currently have "professional work". My goal is to become a military intelligence analyst and I'm sure OCaml will have a place there.

VazScep wrote:It is used for single-dynamic-dispatch (a form of subtyping), which is something that Ocaml's modules cannot do.

Well of course not, they don't have late binding.

But you can, in some sense, "subclass" modules with a functor. I recently needed to key a hash table with pairs of big_ints. Since = chokes on big_ints for some reason, what I did was use the Hashtbl.Make functor to get equal to use eq_big_int

VazScep wrote:In Java, I would need to abstract over constructors, which I can't do. So I end up with a more convoluted design involving two interfaces, one for the returned type and one for the constructing function (typically called an "abstract factory"). Yuck.

Java is really bad.

VazScep wrote:IIn the end, most of the things that got me interested in CL were things that were done just as well if not better in statically typed functional languages. The only thing that left it unique were macros, whose utility I grossly overestimated.

Macros are a shitty form of encapsulation and, from what I'm told, very difficult to debug.

Sigillum Militum wrote:Well of course not, they don't have late binding.

But you can, in some sense, "subclass" modules with a functor. I recently needed to key a hash table with pairs of big_ints. Since = chokes on big_ints for some reason, what I did was use the Hashtbl.Make functor to get equal to use eq_big_int

In Java and C#, this general sort of behaviour is not implemented via subclassing.

Consider how ordered sets are implemented in Ocaml. We have BatSet.Make, which is a functor from a Comparable module to a Set module. In Java and C#, sets are implemented by TreeSet and SortedSet. Before generics, the container type of both collections was Object, and comparison had to be achieved via downcasts to IComparable. This completely type unsafe solution is basically an admission by the language designers that the object system has failed them (due to backwards compatibility issues, the class still relies on downcasts, so the code still isn't typesafe).

With generics, the correct solution can be achieved, but that solution is the Standard ML/Ocaml solution: you make TreeSet a class/module which is parametrised on a type which implements the interface/signature Comparable. Of course, generics were added to Java and C# by Haskell and ML researchers.

If we want to talk about subclassing in the context of modules, we can at least talk about inheritance, which is a standard feature of SML and Ocaml via the "includes" directive. We can also point out that modules can be understood as values with types as their signatures, and that in this way, the module system uses structural subtyping.

On late binding: it isn't always such a big deal when you have first-class functions. A flat class hierarchy, with various classes implementing a single interface, can be captured adequately by a record of functions. If, however, you find yourself writing transformations of these records which remove elements, you should probably be using classes. Suffice to say, I haven't yet come across a need to do this.

Macros are a shitty form of encapsulation and, from what I'm told, very difficult to debug.

I was told macros were a way to turn Common Lisp into a domain-specific language, to bring your solution domain up to meet the problem domain, to give you the ultimate abstraction mechanism, to transcend object-oriented programming, yadda, yadda, yadda. This sort of thing turned out to be bullshit, and most uses of macros that I came across were spurious.

I still consider macros an important and interesting idea, but they need to be seen for exactly what they are: a means of deriving custom syntax.

Being able to derive new syntax requires knowing your language's grammar, its lexemes and tokens, and its abstract syntax. In Lisp, this is wonderfully trivial: Lisp programmers already know their languages abstract syntax and its tokens. The abstract syntax consists in the Lisp s-expressions they write directly, and the tokens are the symbols they use as internalised strings. They also know how to transform abstract syntax, because in learning Lisp, they've become expert at transforming s-expressions. Writing reader macros is similarly trivial.

In Ocaml, if I want to derive new syntax, I have to learn the language and API of Camlp4. I have yet to do this, but it looks like a headache.

This begs the question of whether we want to derive our own syntax. I can only say, judging by the number of camlp4 extensions out there, Ocaml programmers certainly do. And I personally don't want to use lwt or Ocsigen without their syntax extensions.

VazScep wrote:With generics, the correct solution can be achieved, but that solution is the Standard ML/Ocaml solution: you make TreeSet a class/module which is parametrised on a type which implements the interface/signature Comparable. Of course, generics were added to Java and C# by Haskell and ML researchers.

Yeah I guess generics is a more appropriate comparison. Prollum is, I don't use Java or C# or C++ so they didn't come to mind immediately.

VazScep wrote:In Ocaml, if I want to derive new syntax, I have to learn the language and API of Camlp4. I have yet to do this, but it looks like a headache.

One of the best (pseudo-)syntactic modifications is |>, which is two lines in Batteries.

VazScep wrote:1, 1, 2, 3, 5, 8, 13, ...
1, 2, 3, 5, 8, 13, 21, ...

Now if you apply addition vertically, you obviously get the Fibonacci sequence with two elements chopped off the front. In other words:

Code: Select all

fibs = 1 : 1 : zipWith (+) fibs (tail fibs)

Note that the way graph reduction is performed in a lazy language means that evaluation here has the same complexity as the iterative solution.

None of the LISPs available at the time had even proper tail recursion, let alone lazy evaluation.

Is there really just one LISP? I read a series of early articles in the History of Programming Languages on this, and my understanding was that there were many dialects around for decades before CL.

Yes, there were many dialects, but there is commonality between the implementation philosophies of all of them.

There are quite a few pretty pictures that show the relationships:

https://www.google.com/search?tbm=isch& ... amily+tree

Was Scheme the first Lisp with tail recursion?

epepke wrote:People who get really into LISP seem to become hostile to everyone else. So LISP didn't really stay with the times. It sort of lives in its own special world. It doesn't have to be this way at all; this is just what happened. I saw this in one of the posted (by @[color=#CC0000][b]VazSkep,[/b][/color] IIRC) links, arguing that LISP wouldn't help you with Perl, but you shouldn't be doing anything in Perl anyway. This, I think, represents a misunderstanding of what Perl is for and a failure to understand that writing beautiful programs isn't always the right thing to do.

It's funny you should say that, because at the time the guy who wrote it died, I remember reading a lot of people still partially blaming him for the failure of LISP to become popular, because he made their community seem much more hostile to newbies.

VazScep wrote:I'd expect you to be. I've thrown you in at the deep end wearing concrete shoes.

Hah, should have known it was a trap!

Right. Actually, I've used the axiom twice with two different instantiations. Rather than doing the instantiation manually, you might find this function helps:

Code: Select all

-- matchMP ( Γ ⊢ (P → Q) (Δ ⊢ P') attempts to match P with P', and then applies MP.
matchMP :: Theorem String -> Proof -> Proof
matchMP imp ant =
  let antT = concl ant in
    case theoremTerm imp of
      p :=>: q ->
        case match p antT of
          [insts] -> MP (UseTheorem $ instM Var insts imp) ant
          _       -> error "MATCH MP"
      _ -> error "MATCH MP"

This function is like mp, but it will try to instantiate the second argument to make it line up with the first.

Okay, thanks!

VazScep wrote:It might be that you are trying to prove something that is more aptly derived from the exercise theorem. Note though, that it took me 16 proof steps in all to do this.

Well ok, will keep that in mind

VazScep wrote:Yeah, there's a fair bit of work to go. My Bootstrap file is 425 lines of proof.

Hopefully that one proof is much smaller than that...

VazScep wrote:Not sure. I'd struggle to be able to give a definition of computer science and what a computer science degree should entail. At one end, if it's just the professional degree of a programmer, then I guess they should be expected to learn as many trade skills as a mechanical engineer

I wouldn't be able to give that definition either. Computer science falls more within either formal disciplines or engineering than science itself.
But it's just that I feel that if your time in the university has done it's job right, then you should be able to pick up and learn anything new just by yourself. So I think that the teachers should focus more on the languages and tools which make their job showing new concepts easier, even if they are not widely used in the corporate world.

VazScep wrote:Heretic! If it types, it's correct!

Yeah, maybe there's more to this, or maybe less. I'm just trying to think of reasons why Common Lisp was made to be so dynamic.

Sometimes there is no deeper reason than just "because they could and it was easy", and in fact I think that having no distinct types helps a lot here.

VazScep wrote:The sort of security I don't have is security from a malicious programmer, who perhaps used "Obj.magic" to circumvent the type system, or exploited a vulnerability in the Ocaml interpreter, or customised the pretty printer to render his trivial theorem that "1 + 1 = 2" as the statement of Fermat's Last Theorem.

Okay, I see

VazScep wrote:I can imagine a world where we actually start paying people large sums of money to do significant formalisation work. We'll probably have to be more concerned then with cheaters.

Don't get your hopes too high on that though

Sigillum Militum wrote:Was Scheme the first Lisp with tail recursion?

I'm sure that people did proper space-free tail recursion before, but I think Scheme was the first to require it of every implementation.

mizvekov wrote:It's funny you should say that, because at the time the guy who wrote it died, I remember reading a lot of people still partially blaming him for the failure of LISP to become popular, because he made their community seem much more hostile to newbies.

As I don't remember his name, I doubt he was all that influential in whether people liked or disliked LISP.

Another thing: When I was in my first "LISP is really cool," I argued with someone. She said that LISP was a totally hardware-independent language. I pointed out that CAR and CDR stood for "contents of the address/decrement register," which were a specific implementation. There have been some attempts to use FIRST and REST, but they never caught on.

The things that bugged me about LISP was how SNUMS depended on word size and were always shorter than the word size. I think that Scheme is superior in this regard, as it has exact and inexact numbers rather than number type/length.

epepke wrote:As I don't remember his name, I doubt he was all that influential in whether people liked or disliked LISP.

Well he was prominent in the late nineties and early 2000's, when LISP was starting to gain popularity again after the AI winter.
Were you still into LISP by that time?

epepke wrote:Another thing: When I was in my first "LISP is really cool," I argued with someone. She said that LISP was a totally hardware-independent language. I pointed out that CAR and CDR stood for "contents of the address/decrement register," which were a specific implementation. There have been some attempts to use FIRST and REST, but they never caught on.

So, was it common for many implementations at the time that you could overflow the bounds of a list with CDR, or was bounds checking normally to be expected?

epepke wrote:The things that bugged me about LISP was how SNUMS depended on word size and were always shorter than the word size. I think that Scheme is superior in this regard, as it has exact and inexact numbers rather than number type/length.

Why did it have to be shorter than word size, they needed some bits to represent some internal states?

mizvekov wrote:Well he was prominent in the late nineties and early 2000's, when LISP was starting to gain popularity again after the AI winter.
Were you still into LISP by that time?

I still liked it (still do), but I was more interested in getting Scheme with quaternions running.

So, was it common for many implementations at the time that you could overflow the bounds of a list with CDR, or was bounds checking normally to be expected?

Not quite sure what you're asking. It was common for CAR and CDR of NIL to return NIL.

epepke wrote:The things that bugged me about LISP was how SNUMS depended on word size and were always shorter than the word size. I think that Scheme is superior in this regard, as it has exact and inexact numbers rather than number type/length.

Why did it have to be shorter than word size, they needed some bits to represent some internal states?

It was normal to use a single addressing word for everything. In a typical implementation, bit 0 was 0 for a pointer to a dotted pair, and 1 for everything else. With a 32-bit word, SNUMS could, at most, use 31 bits for the number. Typically, it was smaller than that, because you need other bits for atoms, strings, arrays, and so on.

epepke wrote:I still liked it (still do), but I was more interested in getting Scheme with quaternions running.

I see, well Erik was really a CL guy from what I remember.

epepke wrote:Not quite sure what you're asking. It was common for CAR and CDR of NIL to return NIL.

Well that answers my question, but on retrospect I think now that my question was stupid, because lists would be too hard to use otherwise.

epepke wrote:It was normal to use a single addressing word for everything. In a typical implementation, bit 0 was 0 for a pointer to a dotted pair, and 1 for everything else. With a 32-bit word, SNUMS could, at most, use 31 bits for the number. Typically, it was smaller than that, because you need other bits for atoms, strings, arrays, and so on.

Yeah I imagined something like that. Still, unless you were doing some fixed point math with them, 31/30 bits per int is not that bad

On tail-call optimisation, I should mention that Clojure doesn't support it. Last time I checked, neither does Scala. I believe both communities think that this should be an issue solved by the JVM, but I'm not sure if that's likely to happen. If you want to write recursive functions that risk blowing the stack, you are expected to use continuations.

epepke wrote:Another thing: When I was in my first "LISP is really cool," I argued with someone. She said that LISP was a totally hardware-independent language. I pointed out that CAR and CDR stood for "contents of the address/decrement register," which were a specific implementation. There have been some attempts to use FIRST and REST, but they never caught on.

I'd be one of the people arguing against the use of "first" and "rest."

Common Lisp's basic data-structure isn't a list. It's a mutable pair (a cons cell). It happens that cons cells can be used to implement lists, but they can also be used to implement trees, key-value pairs, cyclic graphs, whatever.

Functions such as "first", "second", "third", "nth" and "rest" are functions which interpret a cons cell as a list. The function "assoc" interprets a cons-cell as an association list. The function "copy-tree" interprets it as a tree. "push" interprets it as an imperative stack. "adjoin" interprets it as a set.

On dirty prototype code, I'd start by implementing everything as cons cell and then writing functions with meaningful names to interpret the data-type more abstractly.

VazScep wrote:I'd be one of the people arguing against the use of "first" and "rest."

Common Lisp's basic data-structure isn't a list. It's a mutable pair (a cons cell). It happens that cons cells can be used to implement lists, but they can also be used to implement trees, key-value pairs, cyclic graphs, whatever.

...

None of which speaks well of CAR and CDR, which only have meaning with respect to an obsolete architecture nobody remembers.

@mizvekov Do you have any thoughts about "concepts" in C++?

Regarding Perl and whether no one should use it:

http://c2.com/cgi/wiki?AsFastAsCee

Hmmm. I wrote two pages of Perl that processed several GigaBytes? of input from a pair of major datasets, compared them using a variety of RegularExpressions, compiled a set of comparative totals and statistics from the data, and which executed in about 35 seconds. I'm not sure I could have written that, such that it ran any faster, in CeeLanguage. Granted, it was a Sun E-10k running SolarisOs, but by any standards, grinding through two sets of 13+GB (that's 26+GB total) files and making sense of it in under a minute on anything is good exercise for the eyebrows. And it's an interpreter. [Still shaking my head]