From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Stefan Israelsson Tampe Newsgroups: gmane.lisp.guile.devel Subject: Some guile-unify activities Date: Fri, 6 May 2011 23:18:05 +0200 Message-ID: NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: multipart/alternative; boundary=000e0cdf0f7c99600304a2a206b1 X-Trace: dough.gmane.org 1304716701 24962 80.91.229.12 (6 May 2011 21:18:21 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Fri, 6 May 2011 21:18:21 +0000 (UTC) To: guile-devel Original-X-From: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Fri May 06 23:18:16 2011 Return-path: Envelope-to: guile-devel@m.gmane.org Original-Received: from lists.gnu.org ([140.186.70.17]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1QISPd-0002q4-NZ for guile-devel@m.gmane.org; Fri, 06 May 2011 23:18:14 +0200 Original-Received: from localhost ([::1]:51143 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1QISPd-0003QW-7j for guile-devel@m.gmane.org; Fri, 06 May 2011 17:18:13 -0400 Original-Received: from eggs.gnu.org ([140.186.70.92]:47723) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1QISPZ-0003QG-9q for guile-devel@gnu.org; Fri, 06 May 2011 17:18:10 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1QISPX-0003tl-A9 for guile-devel@gnu.org; Fri, 06 May 2011 17:18:09 -0400 Original-Received: from mail-iy0-f169.google.com ([209.85.210.169]:45611) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1QISPX-0003t3-12 for guile-devel@gnu.org; Fri, 06 May 2011 17:18:07 -0400 Original-Received: by iyh42 with SMTP id 42so4053436iyh.0 for ; Fri, 06 May 2011 14:18:06 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:date:message-id:subject:from:to :content-type; bh=Bck6Jh9Gx+jqvtl+5jkwdKhElGP9gZlEFt3ndnac+bQ=; b=BXlhZJtJDHCEC8A4J5z9pndM/AmwpXxaiR1NedwDiJndDf7Du+2VFqofPUNilWr8F2 zVUfIuJzLNWmx2d7leZW4htTGufJR7f8N227DXedC7yZUu33o8ItPEQ2F7KQTG3E0BfL GlLcjmDcq0LjWzbjEfWmCpjc1L1MmFW738SOQ= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=Bag88Ww4nY36zKzOm1LHvgG/2UxS4WqjzT2srTI2+VtIXD7Uj5V7t+6MGs+O6BMsOD xhXa+9dN7P8Il5wlT5JJpV5bkWy5UROJvCMu+88GRZtcfdju0QY8vsotdi8r/qe59WQ0 i3OYn3bPF+6oXcpX9/DtbKc1ge/A8QfK1Fyxs= Original-Received: by 10.231.82.139 with SMTP id b11mr2524305ibl.134.1304716685958; Fri, 06 May 2011 14:18:05 -0700 (PDT) Original-Received: by 10.231.192.80 with HTTP; Fri, 6 May 2011 14:18:05 -0700 (PDT) X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6 (newer, 2) X-Received-From: 209.85.210.169 X-BeenThere: guile-devel@gnu.org X-Mailman-Version: 2.1.14 Precedence: list List-Id: "Developers list for Guile, the GNU extensibility library" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Original-Sender: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Xref: news.gmane.org gmane.lisp.guile.devel:12447 Archived-At: --000e0cdf0f7c99600304a2a206b1 Content-Type: text/plain; charset=ISO-8859-1 Hi, Just wanted to chime in and tell you a little about what I'm doing with the guile-unify package. First off, this is a tool to do backtracking effectively e.g. tree searches and make heavy use of dynamic variables. There is three activities ongoing. 1. type-checking examples 2. first order logic solvers (porting leanCop) 3. documentation 1. Documentation, I needed to recap somethings and started to improve on the examples above in order to achieve higher generality. As it turned out bug's in the underlying code is squashed all the time and new useful features for the macro package is dicoverwed. So the codebase is in a pretty fluent state still. On the other hand some of the basic features is being documented. 2. The core part of the first order logic leanCop solver has been translated to a macro package and are now in a pure scheme form. It's not that advanced. Then there is a language for how to state the problem especially a translational tool to gather information from a database of first order logic problems. The idea now is to mod that tool into spitting out a file of of the translation which are working then call guile and let guile read in that file and process it with the core solver. The idea is to test out a few alternative solving teqniques and evaluate their performance for the database. 3. For the type-checking examples I've been working with the assumptions of having fixed declarations for lambdas and deduce types for variables and their passage through the system. The thought is that in the end one need to allow lambdas to be explicitly typed in order to allow advanced type-checking and at the same time avoid infinite recursions. I think that it's not uncommon in Haskell programming to add type information in order to guide the type checker and being at such an infant stage having something useful and working must simple allow for type hint's in the code. It would be cool to let emacs interact with guile to give a tool to automagically construct type signatures aka (lambda (A) B) --> (lambda (integer) integer) E.g. be able to interactively deduce a type signature. I will try to add more type primitives like recursive types and so on to be able to match Haskel and typed racket. Generally the biggest problem with backtracking is complexity issues. One can design relatively small programs that makes the type checker work for ages. i will not adress this right now but there are plenty of short cut's to be taken in order to speed up the checker. It would be good if there was a standard way to enter type information in guile and if that information could be hooked into the tree-il representation. But until then I will just use a simple macro framework to enter typed functions. To note below if a lambda produces (or a b) then the rest of the code has to be tried with a and when checked then backtrack and be tried with b if both are type checked then we can proceed. (this is the naive and simple implementation) So we can have a general type checker but complexity wise it will be awful. ------------------------------------------------------------------------------------------- So now this works in 1 sec, ********************** Code (have a geometric explosion in complexity e.g. works like 1000 lines of code) ****************** (tdefine (f X) (type (lambda (boolean) (or integer symbol)) ;; type signature is (type type-desc code ...) and gives a type hint to the lambda (let ((F (lambda (P) (type (lambda (boolean) (or integer symbol)) (if P 1 's))))) (F #t) (F #t) (F #t) (F #t) (F #t) (F #t) (F #t) (F #t) (F #t) (F #f)))) ************************************************** first stage compiled code *********************************** (check (lambda ((#{X\ 10764}# : boolean)) : (or integer symbol) (begin (let #{F\ 10770}# (lambda ((#{P\ 10771}# : boolean)) : (or integer symbol) (begin (if #{P\ 10771}# 1 (quote s)))) (begin (begin (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#t)) (apply #{F\ 10770}# (#f)))))))) ---------------------------------------------------------- **************************************** Deduced Equation ******************************* ((= (lambda #) Tres) ((= #{X\ 10764}# boolean) (= (lambda #) #{F\ 10770}#) ((= #{P\ 10771}# boolean) (or ((= (res #{P\ 10771}#) boolean) (= (res integer) (or integer symbol))) ((= (res #{P\ 10771}#) boolean) (= (res symbol) (or integer symbol))))) (= (res #{F\ 10770}#) (lambda (arg Targ10777) Tres10778)) (= (res boolean) (arg Targ10777)) (= (res Tres10778) A10776) (= (res #{F\ 10770}#) (lambda (arg Targ10780) Tres10781)) (= (res boolean) (arg Targ10780)) (= (res Tres10781) A10779) (= (res #{F\ 10770}#) (lambda (arg Targ10783) Tres10784)) (= (res boolean) (arg Targ10783)) (= (res Tres10784) A10782) (= (res #{F\ 10770}#) (lambda (arg Targ10786) Tres10787)) (= (res boolean) (arg Targ10786)) (= (res Tres10787) A10785) (= (res #{F\ 10770}#) (lambda (arg Targ10789) Tres10790)) (= (res boolean) (arg Targ10789)) (= (res Tres10790) A10788) (= (res #{F\ 10770}#) (lambda (arg Targ10792) Tres10793)) (= (res boolean) (arg Targ10792)) (= (res Tres10793) A10791) (= (res #{F\ 10770}#) (lambda (arg Targ10795) Tres10796)) (= (res boolean) (arg Targ10795)) (= (res Tres10796) A10794) (= (res #{F\ 10770}#) (lambda (arg Targ10798) Tres10799)) (= (res boolean) (arg Targ10798)) (= (res Tres10799) A10797) (= (res #{F\ 10770}#) (lambda (arg Targ10801) Tres10802)) (= (res boolean) (arg Targ10801)) (= (res Tres10802) A10800) (= (res #{F\ 10770}#) (lambda (arg Targ10803) Tres10804)) (= (res boolean) (arg Targ10803)) (= (res Tres10804) (or integer symbol)))) ;;; compiled /home/stis/stis/src/guile/cache/guile/ccache/2.0-0.S-LE-8/home/stis/stis/src/guile/module/language/typed-guile/test.scm.go ************************************************************* Verdict defined f : (lambda (arg boolean) (or integer symbol)) $1 = #t /Stefan --000e0cdf0f7c99600304a2a206b1 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Hi,

Just wanted to chime in and tell you a little about what I'm= doing with the guile-unify package.

First off, this is a tool to do= backtracking effectively e.g. tree searches and make heavy use of
dyna= mic variables.

There is three activities ongoing.

1.=A0 type-checking examples<= br>2.=A0 first order logic solvers (porting leanCop)
3. documentation
1. Documentation, I needed to recap somethings and started to improve = on the examples above in order to achieve
higher generality. As it turned out bug's in the underlying code is squ= ashed all the time and new useful features for the
macro package is dico= verwed. So the codebase is in a pretty fluent state still. On the other han= d some of the basic features
is being documented.

2. The core part of the first order logic leanC= op solver has been translated to a macro package and are now in a pure sche= me form. It's not that
advanced. Then there is a language for how t= o state the problem especially a translational tool to gather information f= rom a
database of first order logic problems. The idea now is to mod that tool in= to spitting out a file of of the translation which are working
then call= guile and let guile read in that file and process it with the core solver.= The idea is to test out a few alternative solving teqniques
and evaluate their performance for the database.

3. For the type-che= cking examples I've been working with the assumptions of having fixed d= eclarations for
lambdas and deduce types for variables and their passage= through the system. The thought is that in the end
one need to allow lambdas to be explicitly typed in order to allow advanced= type-checking and at the same time
avoid infinite recursions. I think t= hat it's not uncommon in Haskell programming to add type information in= order
to guide the type checker and being at such an infant stage having somethin= g useful and working must simple allow
for type hint's in the code.= =A0


It would be cool to let emacs interact with guile to give a= tool to automagically construct
type signatures aka
(lambda (A) B)=A0 <enter>
--> (lambda (i= nteger) integer)

E.g. be able to interactively deduce a type signat= ure.

I will try to add more type primitives like recursive types and= so on to be able to match Haskel and typed racket.
Generally the biggest problem with backtracking is complexity issues. One c= an design relatively small programs
that makes the type checker work fo= r ages. i will not adress this right now but there are plenty of short cut&= #39;s to be taken
in order to speed up the checker.

It would be good if there was a st= andard way to enter type information in guile and if that information could= be hooked into the
tree-il representation. But until then I will just u= se a simple macro framework to enter typed functions.

To note below if a lambda produces (or a b) then the rest of the code h= as to be tried with a and when checked then backtrack and be tried with bif both are type checked then we can proceed. (this is the naive and simp= le implementation)=A0 So we can have a general type checker but complexity = wise
it will be awful.
------------------------------------------------------= -------------------------------------
So now this works in 1 sec,
***= ******************* Code (have a geometric explosion in complexity e.g. wor= ks like 1000 lines of code) ******************
(tdefine (f X)
=A0 (type (lambda (boolean) (or integer symbol))=A0=A0=A0= ;; type signature is (type type-desc code ...) and gives a type hint to th= e lambda
=A0=A0=A0 (let ((F (lambda (P)
=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0 (type (lambda (boolean) (or integer symbol))
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (if P 1 's)))))
=A0= =A0=A0=A0=A0 (F #t)
=A0=A0=A0=A0=A0 (F #t)
=A0=A0=A0=A0=A0 (F #t)
= =A0=A0=A0=A0=A0 (F #t)
=A0=A0=A0=A0=A0 (F #t)
=A0=A0=A0=A0=A0 (F #t)<= br>=A0=A0=A0=A0=A0 (F #t)
=A0=A0=A0=A0=A0 (F #t)
=A0=A0=A0=A0=A0 (F #= t)
=A0=A0=A0=A0=A0 (F #f))))
****************************************= ********** first stage compiled code=A0 ***********************************=
(check (lambda ((#{X\ 10764}# : boolean))
=A0=A0=A0=A0=A0=A0=A0=A0 :
= =A0=A0=A0=A0=A0=A0=A0=A0 (or integer symbol)
=A0=A0=A0=A0=A0=A0=A0=A0 (b= egin
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (let #{F\ 10770}# (lambda
=A0=A0= =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0 ((#{P\ 10771}# : boolean))
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 :
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0 (or integer symbol)
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (begin (if #{P\ 10771}# 1 = (quote s))))
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (begin
=A0=A0=A0=A0= =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (begin
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t))
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t))
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t))<= br>=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t= ))
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# = (#t))
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770= }# (#t))
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10= 770}# (#t))
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t))<= br>=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# (#t= ))
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 (apply #{F\ 10770}# = (#f))))))))
----------------------------------------------------------**************************************** Deduced Equation ***************= ****************
((=3D (lambda #<procedure 2a55800 at language/prolog/typecheck/equationa= lize.scm:72:2 ()>)
=A0=A0=A0 Tres)
=A0((=3D #{X\ 10764}# boolean)<= br>=A0 (=3D (lambda #<procedure 2a55760 at language/prolog/typecheck/equ= ationalize.scm:72:2 ()>)
=A0=A0=A0=A0 #{F\ 10770}#)
=A0 ((=3D #{P\ 10771}# boolean)
=A0=A0 (or= ((=3D (res #{P\ 10771}#) boolean)
=A0=A0=A0=A0=A0=A0=A0 (=3D (res integ= er) (or integer symbol)))
=A0=A0=A0=A0=A0=A0 ((=3D (res #{P\ 10771}#) bo= olean)
=A0=A0=A0=A0=A0=A0=A0 (=3D (res symbol) (or integer symbol))))) =A0 (=3D (res #{F\ 10770}#)
=A0=A0=A0=A0 (lambda (arg Targ10777) Tres107= 78))
=A0 (=3D (res boolean) (arg Targ10777))
=A0 (=3D (res Tres10778)= A10776)
=A0 (=3D (res #{F\ 10770}#)
=A0=A0=A0=A0 (lambda (arg Targ10= 780) Tres10781))
=A0 (=3D (res boolean) (arg Targ10780))
=A0 (=3D (res Tres10781) A10779)
=A0 (=3D (res #{F\ 10770}#)
=A0=A0= =A0=A0 (lambda (arg Targ10783) Tres10784))
=A0 (=3D (res boolean) (arg T= arg10783))
=A0 (=3D (res Tres10784) A10782)
=A0 (=3D (res #{F\ 10770}= #)
=A0=A0=A0=A0 (lambda (arg Targ10786) Tres10787))
=A0 (=3D (res boolean) (arg Targ10786))
=A0 (=3D (res Tres10787) A10785)=
=A0 (=3D (res #{F\ 10770}#)
=A0=A0=A0=A0 (lambda (arg Targ10789) Tre= s10790))
=A0 (=3D (res boolean) (arg Targ10789))
=A0 (=3D (res Tres10= 790) A10788)
=A0 (=3D (res #{F\ 10770}#)
=A0=A0=A0=A0 (lambda (arg Targ10792) Tres10793))
=A0 (=3D (res boolean) = (arg Targ10792))
=A0 (=3D (res Tres10793) A10791)
=A0 (=3D (res #{F\ = 10770}#)
=A0=A0=A0=A0 (lambda (arg Targ10795) Tres10796))
=A0 (=3D (r= es boolean) (arg Targ10795))
=A0 (=3D (res Tres10796) A10794)
=A0 (=3D (res #{F\ 10770}#)
=A0=A0= =A0=A0 (lambda (arg Targ10798) Tres10799))
=A0 (=3D (res boolean) (arg T= arg10798))
=A0 (=3D (res Tres10799) A10797)
=A0 (=3D (res #{F\ 10770}= #)
=A0=A0=A0=A0 (lambda (arg Targ10801) Tres10802))
=A0 (=3D (res boolean) (arg Targ10801))
=A0 (=3D (res Tres10802) A10800)=
=A0 (=3D (res #{F\ 10770}#)
=A0=A0=A0=A0 (lambda (arg Targ10803) Tre= s10804))
=A0 (=3D (res boolean) (arg Targ10803))
=A0 (=3D (res Tres10= 804) (or integer symbol))))
;;; compiled /home/stis/stis/src/guile/cache/guile/ccache/2.0-0.S-LE-8/home= /stis/stis/src/guile/module/language/typed-guile/test.scm.go

*******= ****************************************************** Verdict
defined f= : (lambda (arg boolean) (or integer symbol))
$1 =3D #t

/Stefan
--000e0cdf0f7c99600304a2a206b1--