[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Avoiding variable clashes
From: |
Hans Aberg |
Subject: |
Re: Avoiding variable clashes |
Date: |
Wed, 13 Apr 2011 18:33:13 +0200 |
On 13 Apr 2011, at 18:25, Noah Lavine wrote:
> I think that mechanism is all that Guile uses at present. However, it
> should be general enough to resolve all situations where variables of
> the same name refer to different entities, assuming you set up the
> environments correctly.
>
> Are you planning on implementing a theorem prover for Guile? That would be
> cool.
Or at least having something to experiment with. From Andy's description, it
seems one may merely have to disable the beta-rule.
I wrote on a theorem prover that pushed comparison of clauses into the
unification, admitting unification branching, and doing breadth-first search.
The hard part was resolving variable clashes in substitution.
Hans
- Avoiding variable clashes, Hans Aberg, 2011/04/13
- Re: Avoiding variable clashes, Andy Wingo, 2011/04/13
- Re: Avoiding variable clashes, Hans Aberg, 2011/04/13
- Re: Avoiding variable clashes, Andy Wingo, 2011/04/13
- Re: Avoiding variable clashes, Hans Aberg, 2011/04/13
- Re: Avoiding variable clashes, Noah Lavine, 2011/04/13
- Re: Avoiding variable clashes, Andy Wingo, 2011/04/14
- Re: Avoiding variable clashes, Noah Lavine, 2011/04/14
- Re: Avoiding variable clashes, Andy Wingo, 2011/04/14
- Re: Avoiding variable clashes, Hans Aberg, 2011/04/14